Theorem ldgenpisyslem1 30226

Description: Lemma for ldgenpisys 30229. (Contributed by Thierry Arnoux, 29-Jun-2020.)

Hypotheses

Ref	Expression
dynkin.p	|- P = { s e. ~P ~P O | ( fi ` s ) C_ s }
dynkin.l	|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. s ) ) }
dynkin.o	|- ( ph -> O e. V )
ldgenpisys.e	|- E = |^| { t e. L | T C_ t }
ldgenpisys.1	|- ( ph -> T e. P )
ldgenpisyslem1.1	|- ( ph -> A e. E )

Assertion

Ref	Expression
ldgenpisyslem1	|- ( ph -> { b e. ~P O | ( A i^i b ) e. E } e. L )

Distinct variable groups:   t, s, x, y, L   O, s, t, x   t, P, x, y   L, s   T, s, t, x   ph, t, x   s, b, x, A, t, y   E, b, s, t, x, y   O, b, y   x, V   y, T   ph, y

Allowed substitution hints:   ph( s, b)   P( s, b)   T( b)   L( b)   V( y, t, s, b)

Proof of Theorem ldgenpisyslem1

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssrab2 3687	. . 3 |- { b e. ~P O | ( A i^i b ) e. E } C_ ~P O
2		dynkin.o	. . . 4 |- ( ph -> O e. V )
3		pwexg 4850	. . . 4 |- ( O e. V -> ~P O e. _V )
4		rabexg 4812	. . . 4 |- ( ~P O e. _V -> { b e. ~P O | ( A i^i b ) e. E } e. _V )
5		elpwg 4166	. . . 4 |- ( { b e. ~P O | ( A i^i b ) e. E } e. _V -> ( { b e. ~P O | ( A i^i b ) e. E } e. ~P ~P O <-> { b e. ~P O | ( A i^i b ) e. E } C_ ~P O ) )
6	2, 3, 4, 5	4syl 19	. . 3 |- ( ph -> ( { b e. ~P O | ( A i^i b ) e. E } e. ~P ~P O <-> { b e. ~P O | ( A i^i b ) e. E } C_ ~P O ) )
7	1, 6	mpbiri 248	. 2 |- ( ph -> { b e. ~P O | ( A i^i b ) e. E } e. ~P ~P O )
8		0elpw 4834	. . . . 5 |- (/) e. ~P O
9	8	a1i 11	. . . 4 |- ( ph -> (/) e. ~P O )
10		dynkin.l	. . . . . . . . . . . 12 |- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. s ) ) }
11	10	isldsys 30219	. . . . . . . . . . 11 |- ( t e. L <-> ( t e. ~P ~P O /\ ( (/) e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. t ) ) ) )
12	11	simprbi 480	. . . . . . . . . 10 |- ( t e. L -> ( (/) e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. t ) ) )
13	12	simp1d 1073	. . . . . . . . 9 |- ( t e. L -> (/) e. t )
14	13	ad2antlr 763	. . . . . . . 8 |- ( ( ( ph /\ t e. L ) /\ T C_ t ) -> (/) e. t )
15	14	ex 450	. . . . . . 7 |- ( ( ph /\ t e. L ) -> ( T C_ t -> (/) e. t ) )
16	15	ralrimiva 2966	. . . . . 6 |- ( ph -> A. t e. L ( T C_ t -> (/) e. t ) )
17		0ex 4790	. . . . . . 7 |- (/) e. _V
18	17	elintrab 4488	. . . . . 6 |- ( (/) e. |^| { t e. L | T C_ t } <-> A. t e. L ( T C_ t -> (/) e. t ) )
19	16, 18	sylibr 224	. . . . 5 |- ( ph -> (/) e. |^| { t e. L | T C_ t } )
20		in0 3968	. . . . 5 |- ( A i^i (/) ) = (/)
21		ldgenpisys.e	. . . . 5 |- E = |^| { t e. L | T C_ t }
22	19, 20, 21	3eltr4g 2718	. . . 4 |- ( ph -> ( A i^i (/) ) e. E )
23		ineq2 3808	. . . . . 6 |- ( b = (/) -> ( A i^i b ) = ( A i^i (/) ) )
24	23	eleq1d 2686	. . . . 5 |- ( b = (/) -> ( ( A i^i b ) e. E <-> ( A i^i (/) ) e. E ) )
25	24	elrab 3363	. . . 4 |- ( (/) e. { b e. ~P O | ( A i^i b ) e. E } <-> ( (/) e. ~P O /\ ( A i^i (/) ) e. E ) )
26	9, 22, 25	sylanbrc 698	. . 3 |- ( ph -> (/) e. { b e. ~P O | ( A i^i b ) e. E } )
27		ineq2 3808	. . . . . . . 8 |- ( b = x -> ( A i^i b ) = ( A i^i x ) )
28	27	eleq1d 2686	. . . . . . 7 |- ( b = x -> ( ( A i^i b ) e. E <-> ( A i^i x ) e. E ) )
29	28	elrab 3363	. . . . . 6 |- ( x e. { b e. ~P O | ( A i^i b ) e. E } <-> ( x e. ~P O /\ ( A i^i x ) e. E ) )
30		pwidg 4173	. . . . . . . . . 10 |- ( O e. V -> O e. ~P O )
31	2, 30	syl 17	. . . . . . . . 9 |- ( ph -> O e. ~P O )
32	31	adantr 481	. . . . . . . 8 |- ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) -> O e. ~P O )
33	32	elpwdifcl 29358	. . . . . . 7 |- ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) -> ( O \ x ) e. ~P O )
34	10	pwldsys 30220	. . . . . . . . . . . . . . . . . . 19 |- ( O e. V -> ~P O e. L )
35	2, 34	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ~P O e. L )
36		ldgenpisys.1	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> T e. P )
37		dynkin.p	. . . . . . . . . . . . . . . . . . . . . 22 |- P = { s e. ~P ~P O | ( fi ` s ) C_ s }
38	37	ispisys 30215	. . . . . . . . . . . . . . . . . . . . 21 |- ( T e. P <-> ( T e. ~P ~P O /\ ( fi ` T ) C_ T ) )
39	36, 38	sylib 208	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( T e. ~P ~P O /\ ( fi ` T ) C_ T ) )
40	39	simpld 475	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> T e. ~P ~P O )
41	40	elpwid 4170	. . . . . . . . . . . . . . . . . 18 |- ( ph -> T C_ ~P O )
42		sseq2 3627	. . . . . . . . . . . . . . . . . . 19 |- ( t = ~P O -> ( T C_ t <-> T C_ ~P O ) )
43	42	intminss 4503	. . . . . . . . . . . . . . . . . 18 |- ( ( ~P O e. L /\ T C_ ~P O ) -> |^| { t e. L | T C_ t } C_ ~P O )
44	35, 41, 43	syl2anc 693	. . . . . . . . . . . . . . . . 17 |- ( ph -> |^| { t e. L | T C_ t } C_ ~P O )
45	21, 44	syl5eqss 3649	. . . . . . . . . . . . . . . 16 |- ( ph -> E C_ ~P O )
46		ldgenpisyslem1.1	. . . . . . . . . . . . . . . 16 |- ( ph -> A e. E )
47	45, 46	sseldd 3604	. . . . . . . . . . . . . . 15 |- ( ph -> A e. ~P O )
48	47	elpwid 4170	. . . . . . . . . . . . . 14 |- ( ph -> A C_ O )
49	48	ad3antrrr 766	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> A C_ O )
50		difin 3861	. . . . . . . . . . . . . . . 16 |- ( A \ ( A i^i x ) ) = ( A \ x )
51		difin2 3890	. . . . . . . . . . . . . . . 16 |- ( A C_ O -> ( A \ x ) = ( ( O \ x ) i^i A ) )
52	50, 51	syl5eq 2668	. . . . . . . . . . . . . . 15 |- ( A C_ O -> ( A \ ( A i^i x ) ) = ( ( O \ x ) i^i A ) )
53		incom 3805	. . . . . . . . . . . . . . 15 |- ( ( O \ x ) i^i A ) = ( A i^i ( O \ x ) )
54	52, 53	syl6eq 2672	. . . . . . . . . . . . . 14 |- ( A C_ O -> ( A \ ( A i^i x ) ) = ( A i^i ( O \ x ) ) )
55		difuncomp 29369	. . . . . . . . . . . . . 14 |- ( A C_ O -> ( A \ ( A i^i x ) ) = ( O \ ( ( O \ A ) u. ( A i^i x ) ) ) )
56	54, 55	eqtr3d 2658	. . . . . . . . . . . . 13 |- ( A C_ O -> ( A i^i ( O \ x ) ) = ( O \ ( ( O \ A ) u. ( A i^i x ) ) ) )
57	49, 56	syl 17	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> ( A i^i ( O \ x ) ) = ( O \ ( ( O \ A ) u. ( A i^i x ) ) ) )
58		difeq2 3722	. . . . . . . . . . . . . 14 |- ( y = ( ( O \ A ) u. ( A i^i x ) ) -> ( O \ y ) = ( O \ ( ( O \ A ) u. ( A i^i x ) ) ) )
59	58	eleq1d 2686	. . . . . . . . . . . . 13 |- ( y = ( ( O \ A ) u. ( A i^i x ) ) -> ( ( O \ y ) e. t <-> ( O \ ( ( O \ A ) u. ( A i^i x ) ) ) e. t ) )
60	12	simp2d 1074	. . . . . . . . . . . . . . 15 |- ( t e. L -> A. x e. t ( O \ x ) e. t )
61	60	ad2antlr 763	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> A. x e. t ( O \ x ) e. t )
62		difeq2 3722	. . . . . . . . . . . . . . . 16 |- ( x = y -> ( O \ x ) = ( O \ y ) )
63	62	eleq1d 2686	. . . . . . . . . . . . . . 15 |- ( x = y -> ( ( O \ x ) e. t <-> ( O \ y ) e. t ) )
64	63	cbvralv 3171	. . . . . . . . . . . . . 14 |- ( A. x e. t ( O \ x ) e. t <-> A. y e. t ( O \ y ) e. t )
65	61, 64	sylib 208	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> A. y e. t ( O \ y ) e. t )
66		simplr 792	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> t e. L )
67	46, 21	syl6eleq 2711	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A e. |^| { t e. L | T C_ t } )
68		elintrabg 4489	. . . . . . . . . . . . . . . . . . . 20 |- ( A e. E -> ( A e. |^| { t e. L | T C_ t } <-> A. t e. L ( T C_ t -> A e. t ) ) )
69	46, 68	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( A e. |^| { t e. L | T C_ t } <-> A. t e. L ( T C_ t -> A e. t ) ) )
70	67, 69	mpbid 222	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A. t e. L ( T C_ t -> A e. t ) )
71	70	r19.21bi 2932	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ t e. L ) -> ( T C_ t -> A e. t ) )
72	71	imp 445	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ t e. L ) /\ T C_ t ) -> A e. t )
73	72	adantllr 755	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> A e. t )
74		difeq2 3722	. . . . . . . . . . . . . . . . 17 |- ( x = A -> ( O \ x ) = ( O \ A ) )
75	74	eleq1d 2686	. . . . . . . . . . . . . . . 16 |- ( x = A -> ( ( O \ x ) e. t <-> ( O \ A ) e. t ) )
76	60	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( t e. L /\ A e. t ) -> A. x e. t ( O \ x ) e. t )
77		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( t e. L /\ A e. t ) -> A e. t )
78	75, 76, 77	rspcdva 3316	. . . . . . . . . . . . . . 15 |- ( ( t e. L /\ A e. t ) -> ( O \ A ) e. t )
79	66, 73, 78	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> ( O \ A ) e. t )
80		simpllr 799	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> ( x e. ~P O /\ ( A i^i x ) e. E ) )
81	80	simprd 479	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> ( A i^i x ) e. E )
82	81, 21	syl6eleq 2711	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> ( A i^i x ) e. |^| { t e. L | T C_ t } )
83		vex 3203	. . . . . . . . . . . . . . . . . 18 |- x e. _V
84	83	inex2 4800	. . . . . . . . . . . . . . . . 17 |- ( A i^i x ) e. _V
85		elintrabg 4489	. . . . . . . . . . . . . . . . 17 |- ( ( A i^i x ) e. _V -> ( ( A i^i x ) e. |^| { t e. L | T C_ t } <-> A. t e. L ( T C_ t -> ( A i^i x ) e. t ) ) )
86	84, 85	mp1i 13	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> ( ( A i^i x ) e. |^| { t e. L | T C_ t } <-> A. t e. L ( T C_ t -> ( A i^i x ) e. t ) ) )
87	82, 86	mpbid 222	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> A. t e. L ( T C_ t -> ( A i^i x ) e. t ) )
88		simpr 477	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> T C_ t )
89		rspa 2930	. . . . . . . . . . . . . . . 16 |- ( ( A. t e. L ( T C_ t -> ( A i^i x ) e. t ) /\ t e. L ) -> ( T C_ t -> ( A i^i x ) e. t ) )
90	89	imp 445	. . . . . . . . . . . . . . 15 |- ( ( ( A. t e. L ( T C_ t -> ( A i^i x ) e. t ) /\ t e. L ) /\ T C_ t ) -> ( A i^i x ) e. t )
91	87, 66, 88, 90	syl21anc 1325	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> ( A i^i x ) e. t )
92		incom 3805	. . . . . . . . . . . . . . . 16 |- ( ( O \ A ) i^i ( A i^i x ) ) = ( ( A i^i x ) i^i ( O \ A ) )
93		inss1 3833	. . . . . . . . . . . . . . . . 17 |- ( A i^i x ) C_ A
94		disjdif 4040	. . . . . . . . . . . . . . . . 17 |- ( A i^i ( O \ A ) ) = (/)
95		ssdisj 4026	. . . . . . . . . . . . . . . . 17 |- ( ( ( A i^i x ) C_ A /\ ( A i^i ( O \ A ) ) = (/) ) -> ( ( A i^i x ) i^i ( O \ A ) ) = (/) )
96	93, 94, 95	mp2an 708	. . . . . . . . . . . . . . . 16 |- ( ( A i^i x ) i^i ( O \ A ) ) = (/)
97	92, 96	eqtri 2644	. . . . . . . . . . . . . . 15 |- ( ( O \ A ) i^i ( A i^i x ) ) = (/)
98	97	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> ( ( O \ A ) i^i ( A i^i x ) ) = (/) )
99	10, 66, 79, 91, 98	unelldsys 30221	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> ( ( O \ A ) u. ( A i^i x ) ) e. t )
100	59, 65, 99	rspcdva 3316	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> ( O \ ( ( O \ A ) u. ( A i^i x ) ) ) e. t )
101	57, 100	eqeltrd 2701	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> ( A i^i ( O \ x ) ) e. t )
102	101	ex 450	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) -> ( T C_ t -> ( A i^i ( O \ x ) ) e. t ) )
103	102	ralrimiva 2966	. . . . . . . . 9 |- ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) -> A. t e. L ( T C_ t -> ( A i^i ( O \ x ) ) e. t ) )
104		inex1g 4801	. . . . . . . . . . . 12 |- ( A e. E -> ( A i^i ( O \ x ) ) e. _V )
105	46, 104	syl 17	. . . . . . . . . . 11 |- ( ph -> ( A i^i ( O \ x ) ) e. _V )
106	105	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) -> ( A i^i ( O \ x ) ) e. _V )
107		elintrabg 4489	. . . . . . . . . 10 |- ( ( A i^i ( O \ x ) ) e. _V -> ( ( A i^i ( O \ x ) ) e. |^| { t e. L | T C_ t } <-> A. t e. L ( T C_ t -> ( A i^i ( O \ x ) ) e. t ) ) )
108	106, 107	syl 17	. . . . . . . . 9 |- ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) -> ( ( A i^i ( O \ x ) ) e. |^| { t e. L | T C_ t } <-> A. t e. L ( T C_ t -> ( A i^i ( O \ x ) ) e. t ) ) )
109	103, 108	mpbird 247	. . . . . . . 8 |- ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) -> ( A i^i ( O \ x ) ) e. |^| { t e. L | T C_ t } )
110	109, 21	syl6eleqr 2712	. . . . . . 7 |- ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) -> ( A i^i ( O \ x ) ) e. E )
111	33, 110	jca 554	. . . . . 6 |- ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) -> ( ( O \ x ) e. ~P O /\ ( A i^i ( O \ x ) ) e. E ) )
112	29, 111	sylan2b 492	. . . . 5 |- ( ( ph /\ x e. { b e. ~P O | ( A i^i b ) e. E } ) -> ( ( O \ x ) e. ~P O /\ ( A i^i ( O \ x ) ) e. E ) )
113		ineq2 3808	. . . . . . 7 |- ( b = ( O \ x ) -> ( A i^i b ) = ( A i^i ( O \ x ) ) )
114	113	eleq1d 2686	. . . . . 6 |- ( b = ( O \ x ) -> ( ( A i^i b ) e. E <-> ( A i^i ( O \ x ) ) e. E ) )
115	114	elrab 3363	. . . . 5 |- ( ( O \ x ) e. { b e. ~P O | ( A i^i b ) e. E } <-> ( ( O \ x ) e. ~P O /\ ( A i^i ( O \ x ) ) e. E ) )
116	112, 115	sylibr 224	. . . 4 |- ( ( ph /\ x e. { b e. ~P O | ( A i^i b ) e. E } ) -> ( O \ x ) e. { b e. ~P O | ( A i^i b ) e. E } )
117	116	ralrimiva 2966	. . 3 |- ( ph -> A. x e. { b e. ~P O | ( A i^i b ) e. E } ( O \ x ) e. { b e. ~P O | ( A i^i b ) e. E } )
118	2	ad2antrr 762	. . . . . . 7 |- ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) -> O e. V )
119		sspwb 4917	. . . . . . . . 9 |- ( { b e. ~P O | ( A i^i b ) e. E } C_ ~P O <-> ~P { b e. ~P O | ( A i^i b ) e. E } C_ ~P ~P O )
120	1, 119	mpbi 220	. . . . . . . 8 |- ~P { b e. ~P O | ( A i^i b ) e. E } C_ ~P ~P O
121		simplr 792	. . . . . . . 8 |- ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) -> x e. ~P { b e. ~P O | ( A i^i b ) e. E } )
122	120, 121	sseldi 3601	. . . . . . 7 |- ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) -> x e. ~P ~P O )
123	118, 122	elpwunicl 29371	. . . . . 6 |- ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) -> U. x e. ~P O )
124		uniin2 29368	. . . . . . . . . . . 12 |- U_ y e. x ( A i^i y ) = ( A i^i U. x )
125		vex 3203	. . . . . . . . . . . . . 14 |- y e. _V
126	125	inex2 4800	. . . . . . . . . . . . 13 |- ( A i^i y ) e. _V
127	126	dfiun3 5380	. . . . . . . . . . . 12 |- U_ y e. x ( A i^i y ) = U. ran ( y e. x |-> ( A i^i y ) )
128	124, 127	eqtr3i 2646	. . . . . . . . . . 11 |- ( A i^i U. x ) = U. ran ( y e. x |-> ( A i^i y ) )
129		simplr 792	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) -> t e. L )
130		nfv 1843	. . . . . . . . . . . . . . . . . 18 |- F/ y ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } )
131		nfv 1843	. . . . . . . . . . . . . . . . . . 19 |- F/ y x ~<_ om
132		nfdisj1 4633	. . . . . . . . . . . . . . . . . . 19 |- F/ yDisj y e. x y
133	131, 132	nfan 1828	. . . . . . . . . . . . . . . . . 18 |- F/ y ( x ~<_ om /\ Disj y e. x y )
134	130, 133	nfan 1828	. . . . . . . . . . . . . . . . 17 |- F/ y ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) )
135		nfv 1843	. . . . . . . . . . . . . . . . 17 |- F/ y t e. L
136	134, 135	nfan 1828	. . . . . . . . . . . . . . . 16 |- F/ y ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L )
137		nfv 1843	. . . . . . . . . . . . . . . 16 |- F/ y T C_ t
138	136, 137	nfan 1828	. . . . . . . . . . . . . . 15 |- F/ y ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t )
139		elpwi 4168	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ~P { b e. ~P O | ( A i^i b ) e. E } -> x C_ { b e. ~P O | ( A i^i b ) e. E } )
140	139	ad4antlr 769	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) -> x C_ { b e. ~P O | ( A i^i b ) e. E } )
141	140	sselda 3603	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) /\ y e. x ) -> y e. { b e. ~P O | ( A i^i b ) e. E } )
142		ineq2 3808	. . . . . . . . . . . . . . . . . . . . 21 |- ( b = y -> ( A i^i b ) = ( A i^i y ) )
143	142	eleq1d 2686	. . . . . . . . . . . . . . . . . . . 20 |- ( b = y -> ( ( A i^i b ) e. E <-> ( A i^i y ) e. E ) )
144	143	elrab 3363	. . . . . . . . . . . . . . . . . . 19 |- ( y e. { b e. ~P O | ( A i^i b ) e. E } <-> ( y e. ~P O /\ ( A i^i y ) e. E ) )
145	144	simprbi 480	. . . . . . . . . . . . . . . . . 18 |- ( y e. { b e. ~P O | ( A i^i b ) e. E } -> ( A i^i y ) e. E )
146	141, 145	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) /\ y e. x ) -> ( A i^i y ) e. E )
147		simpllr 799	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) /\ y e. x ) -> t e. L )
148		simplr 792	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) /\ y e. x ) -> T C_ t )
149	21	eleq2i 2693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A i^i y ) e. E <-> ( A i^i y ) e. |^| { t e. L | T C_ t } )
150	126	elintrab 4488	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A i^i y ) e. |^| { t e. L | T C_ t } <-> A. t e. L ( T C_ t -> ( A i^i y ) e. t ) )
151	149, 150	bitri 264	. . . . . . . . . . . . . . . . . . 19 |- ( ( A i^i y ) e. E <-> A. t e. L ( T C_ t -> ( A i^i y ) e. t ) )
152		rspa 2930	. . . . . . . . . . . . . . . . . . 19 |- ( ( A. t e. L ( T C_ t -> ( A i^i y ) e. t ) /\ t e. L ) -> ( T C_ t -> ( A i^i y ) e. t ) )
153	151, 152	sylanb 489	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A i^i y ) e. E /\ t e. L ) -> ( T C_ t -> ( A i^i y ) e. t ) )
154	153	imp 445	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( A i^i y ) e. E /\ t e. L ) /\ T C_ t ) -> ( A i^i y ) e. t )
155	146, 147, 148, 154	syl21anc 1325	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) /\ y e. x ) -> ( A i^i y ) e. t )
156	155	ex 450	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) -> ( y e. x -> ( A i^i y ) e. t ) )
157	138, 156	ralrimi 2957	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) -> A. y e. x ( A i^i y ) e. t )
158		eqid 2622	. . . . . . . . . . . . . . 15 |- ( y e. x |-> ( A i^i y ) ) = ( y e. x |-> ( A i^i y ) )
159	158	rnmptss 6392	. . . . . . . . . . . . . 14 |- ( A. y e. x ( A i^i y ) e. t -> ran ( y e. x |-> ( A i^i y ) ) C_ t )
160	157, 159	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) -> ran ( y e. x |-> ( A i^i y ) ) C_ t )
161	129, 160	sselpwd 4807	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) -> ran ( y e. x |-> ( A i^i y ) ) e. ~P t )
162		simpllr 799	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) -> ( x ~<_ om /\ Disj y e. x y ) )
163	162	simpld 475	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) -> x ~<_ om )
164		1stcrestlem 21255	. . . . . . . . . . . . 13 |- ( x ~<_ om -> ran ( y e. x |-> ( A i^i y ) ) ~<_ om )
165	163, 164	syl 17	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) -> ran ( y e. x |-> ( A i^i y ) ) ~<_ om )
166	162	simprd 479	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) -> Disj y e. x y )
167		disjin2 29400	. . . . . . . . . . . . . 14 |- (Disj y e. x y -> Disj y e. x ( A i^i y ) )
168		disjrnmpt 29398	. . . . . . . . . . . . . 14 |- (Disj y e. x ( A i^i y ) -> Disj z e. ran ( y e. x |-> ( A i^i y ) ) z )
169	166, 167, 168	3syl 18	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) -> Disj z e. ran ( y e. x |-> ( A i^i y ) ) z )
170		nfmpt1 4747	. . . . . . . . . . . . . . 15 |- F/_ y ( y e. x |-> ( A i^i y ) )
171	170	nfrn 5368	. . . . . . . . . . . . . 14 |- F/_ y ran ( y e. x |-> ( A i^i y ) )
172		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ z y
173		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ y z
174		id 22	. . . . . . . . . . . . . 14 |- ( y = z -> y = z )
175	171, 172, 173, 174	cbvdisjf 29385	. . . . . . . . . . . . 13 |- (Disj y e. ran ( y e. x |-> ( A i^i y ) ) y <-> Disj z e. ran ( y e. x |-> ( A i^i y ) ) z )
176	169, 175	sylibr 224	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) -> Disj y e. ran ( y e. x |-> ( A i^i y ) ) y )
177		breq1 4656	. . . . . . . . . . . . . . . 16 |- ( z = ran ( y e. x |-> ( A i^i y ) ) -> ( z ~<_ om <-> ran ( y e. x |-> ( A i^i y ) ) ~<_ om ) )
178	173, 171	disjeq1f 29387	. . . . . . . . . . . . . . . 16 |- ( z = ran ( y e. x |-> ( A i^i y ) ) -> (Disj y e. z y <-> Disj y e. ran ( y e. x |-> ( A i^i y ) ) y ) )
179	177, 178	anbi12d 747	. . . . . . . . . . . . . . 15 |- ( z = ran ( y e. x |-> ( A i^i y ) ) -> ( ( z ~<_ om /\ Disj y e. z y ) <-> ( ran ( y e. x |-> ( A i^i y ) ) ~<_ om /\ Disj y e. ran ( y e. x |-> ( A i^i y ) ) y ) ) )
180		unieq 4444	. . . . . . . . . . . . . . . 16 |- ( z = ran ( y e. x |-> ( A i^i y ) ) -> U. z = U. ran ( y e. x |-> ( A i^i y ) ) )
181	180	eleq1d 2686	. . . . . . . . . . . . . . 15 |- ( z = ran ( y e. x |-> ( A i^i y ) ) -> ( U. z e. t <-> U. ran ( y e. x |-> ( A i^i y ) ) e. t ) )
182	179, 181	imbi12d 334	. . . . . . . . . . . . . 14 |- ( z = ran ( y e. x |-> ( A i^i y ) ) -> ( ( ( z ~<_ om /\ Disj y e. z y ) -> U. z e. t ) <-> ( ( ran ( y e. x |-> ( A i^i y ) ) ~<_ om /\ Disj y e. ran ( y e. x |-> ( A i^i y ) ) y ) -> U. ran ( y e. x |-> ( A i^i y ) ) e. t ) ) )
183	12	simp3d 1075	. . . . . . . . . . . . . . . 16 |- ( t e. L -> A. x e. ~P t ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. t ) )
184		breq1 4656	. . . . . . . . . . . . . . . . . . 19 |- ( x = z -> ( x ~<_ om <-> z ~<_ om ) )
185		disjeq1 4627	. . . . . . . . . . . . . . . . . . 19 |- ( x = z -> (Disj y e. x y <-> Disj y e. z y ) )
186	184, 185	anbi12d 747	. . . . . . . . . . . . . . . . . 18 |- ( x = z -> ( ( x ~<_ om /\ Disj y e. x y ) <-> ( z ~<_ om /\ Disj y e. z y ) ) )
187		unieq 4444	. . . . . . . . . . . . . . . . . . 19 |- ( x = z -> U. x = U. z )
188	187	eleq1d 2686	. . . . . . . . . . . . . . . . . 18 |- ( x = z -> ( U. x e. t <-> U. z e. t ) )
189	186, 188	imbi12d 334	. . . . . . . . . . . . . . . . 17 |- ( x = z -> ( ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. t ) <-> ( ( z ~<_ om /\ Disj y e. z y ) -> U. z e. t ) ) )
190	189	cbvralv 3171	. . . . . . . . . . . . . . . 16 |- ( A. x e. ~P t ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. t ) <-> A. z e. ~P t ( ( z ~<_ om /\ Disj y e. z y ) -> U. z e. t ) )
191	183, 190	sylib 208	. . . . . . . . . . . . . . 15 |- ( t e. L -> A. z e. ~P t ( ( z ~<_ om /\ Disj y e. z y ) -> U. z e. t ) )
192	191	adantr 481	. . . . . . . . . . . . . 14 |- ( ( t e. L /\ ran ( y e. x |-> ( A i^i y ) ) e. ~P t ) -> A. z e. ~P t ( ( z ~<_ om /\ Disj y e. z y ) -> U. z e. t ) )
193		simpr 477	. . . . . . . . . . . . . 14 |- ( ( t e. L /\ ran ( y e. x |-> ( A i^i y ) ) e. ~P t ) -> ran ( y e. x |-> ( A i^i y ) ) e. ~P t )
194	182, 192, 193	rspcdva 3316	. . . . . . . . . . . . 13 |- ( ( t e. L /\ ran ( y e. x |-> ( A i^i y ) ) e. ~P t ) -> ( ( ran ( y e. x |-> ( A i^i y ) ) ~<_ om /\ Disj y e. ran ( y e. x |-> ( A i^i y ) ) y ) -> U. ran ( y e. x |-> ( A i^i y ) ) e. t ) )
195	194	imp 445	. . . . . . . . . . . 12 |- ( ( ( t e. L /\ ran ( y e. x |-> ( A i^i y ) ) e. ~P t ) /\ ( ran ( y e. x |-> ( A i^i y ) ) ~<_ om /\ Disj y e. ran ( y e. x |-> ( A i^i y ) ) y ) ) -> U. ran ( y e. x |-> ( A i^i y ) ) e. t )
196	129, 161, 165, 176, 195	syl22anc 1327	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) -> U. ran ( y e. x |-> ( A i^i y ) ) e. t )
197	128, 196	syl5eqel 2705	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) /\ T C_ t ) -> ( A i^i U. x ) e. t )
198	197	ex 450	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) /\ t e. L ) -> ( T C_ t -> ( A i^i U. x ) e. t ) )
199	198	ralrimiva 2966	. . . . . . . 8 |- ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) -> A. t e. L ( T C_ t -> ( A i^i U. x ) e. t ) )
200		vuniex 6954	. . . . . . . . . 10 |- U. x e. _V
201	200	inex2 4800	. . . . . . . . 9 |- ( A i^i U. x ) e. _V
202	201	elintrab 4488	. . . . . . . 8 |- ( ( A i^i U. x ) e. |^| { t e. L | T C_ t } <-> A. t e. L ( T C_ t -> ( A i^i U. x ) e. t ) )
203	199, 202	sylibr 224	. . . . . . 7 |- ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) -> ( A i^i U. x ) e. |^| { t e. L | T C_ t } )
204	203, 21	syl6eleqr 2712	. . . . . 6 |- ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) -> ( A i^i U. x ) e. E )
205		ineq2 3808	. . . . . . . 8 |- ( b = U. x -> ( A i^i b ) = ( A i^i U. x ) )
206	205	eleq1d 2686	. . . . . . 7 |- ( b = U. x -> ( ( A i^i b ) e. E <-> ( A i^i U. x ) e. E ) )
207	206	elrab 3363	. . . . . 6 |- ( U. x e. { b e. ~P O | ( A i^i b ) e. E } <-> ( U. x e. ~P O /\ ( A i^i U. x ) e. E ) )
208	123, 204, 207	sylanbrc 698	. . . . 5 |- ( ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ om /\ Disj y e. x y ) ) -> U. x e. { b e. ~P O | ( A i^i b ) e. E } )
209	208	ex 450	. . . 4 |- ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) -> ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. { b e. ~P O | ( A i^i b ) e. E } ) )
210	209	ralrimiva 2966	. . 3 |- ( ph -> A. x e. ~P { b e. ~P O | ( A i^i b ) e. E } ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. { b e. ~P O | ( A i^i b ) e. E } ) )
211	26, 117, 210	3jca 1242	. 2 |- ( ph -> ( (/) e. { b e. ~P O | ( A i^i b ) e. E } /\ A. x e. { b e. ~P O | ( A i^i b ) e. E } ( O \ x ) e. { b e. ~P O | ( A i^i b ) e. E } /\ A. x e. ~P { b e. ~P O | ( A i^i b ) e. E } ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. { b e. ~P O | ( A i^i b ) e. E } ) ) )
212	10	isldsys 30219	. 2 |- ( { b e. ~P O | ( A i^i b ) e. E } e. L <-> ( { b e. ~P O | ( A i^i b ) e. E } e. ~P ~P O /\ ( (/) e. { b e. ~P O | ( A i^i b ) e. E } /\ A. x e. { b e. ~P O | ( A i^i b ) e. E } ( O \ x ) e. { b e. ~P O | ( A i^i b ) e. E } /\ A. x e. ~P { b e. ~P O | ( A i^i b ) e. E } ( ( x ~<_ om /\ Disj y e. x y ) -> U. x e. { b e. ~P O | ( A i^i b ) e. E } ) ) ) )
213	7, 211, 212	sylanbrc 698	1 |- ( ph -> { b e. ~P O | ( A i^i b ) e. E } e. L )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   {crab 2916   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   U.cuni 4436   |^|cint 4475   U_ciun 4520  Disj wdisj 4620   class class class wbr 4653   |-> cmpt 4729   ran crn 5115   ` cfv 5888   omcom 7065   ~<_ cdom 7953   ficfi 8316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-disj 4621  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-oi 8415  df-card 8765  df-acn 8768  df-cda 8990

This theorem is referenced by:  ldgenpisyslem2  30227