Metamath Proof Explorer

Theorem ldgenpisyslem1

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

Ref Expression
Hypotheses 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 ldgenpisyslem1 
|- ( ph -> { b e. ~P O | ( A i^i b ) e. E } e. L )

Proof

Step Hyp Ref Expression
1 dynkin.p 
 |-  P = { s e. ~P ~P O | ( fi ` s ) C_ s }
2 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 ) ) }
3 dynkin.o 
 |-  ( ph -> O e. V )
4 ldgenpisys.e 
 |-  E = |^| { t e. L | T C_ t }
5 ldgenpisys.1 
 |-  ( ph -> T e. P )
6 ldgenpisyslem1.1 
 |-  ( ph -> A e. E )
7 ssrab2 
 |-  { b e. ~P O | ( A i^i b ) e. E } C_ ~P O
8 pwexg 
 |-  ( O e. V -> ~P O e. _V )
9 rabexg 
 |-  ( ~P O e. _V -> { b e. ~P O | ( A i^i b ) e. E } e. _V )
10 elpwg 
 |-  ( { 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 ) )
11 3 8 9 10 4syl 
 |-  ( 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 ) )
12 7 11 mpbiri 
 |-  ( ph -> { b e. ~P O | ( A i^i b ) e. E } e. ~P ~P O )
13 ineq2 
 |-  ( b = (/) -> ( A i^i b ) = ( A i^i (/) ) )
14 13 eleq1d 
 |-  ( b = (/) -> ( ( A i^i b ) e. E <-> ( A i^i (/) ) e. E ) )
15 0elpw 
 |-  (/) e. ~P O
16 15 a1i 
 |-  ( ph -> (/) e. ~P O )
17 2 isldsys 
 |-  ( 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 ) ) ) )
18 17 simprbi 
 |-  ( 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 ) ) )
19 18 simp1d 
 |-  ( t e. L -> (/) e. t )
20 19 ad2antlr 
 |-  ( ( ( ph /\ t e. L ) /\ T C_ t ) -> (/) e. t )
21 20 ex 
 |-  ( ( ph /\ t e. L ) -> ( T C_ t -> (/) e. t ) )
22 21 ralrimiva 
 |-  ( ph -> A. t e. L ( T C_ t -> (/) e. t ) )
23 0ex 
 |-  (/) e. _V
24 23 elintrab 
 |-  ( (/) e. |^| { t e. L | T C_ t } <-> A. t e. L ( T C_ t -> (/) e. t ) )
25 22 24 sylibr 
 |-  ( ph -> (/) e. |^| { t e. L | T C_ t } )
26 in0 
 |-  ( A i^i (/) ) = (/)
27 25 26 4 3eltr4g 
 |-  ( ph -> ( A i^i (/) ) e. E )
28 14 16 27 elrabd 
 |-  ( ph -> (/) e. { b e. ~P O | ( A i^i b ) e. E } )
29 ineq2 
 |-  ( b = x -> ( A i^i b ) = ( A i^i x ) )
30 29 eleq1d 
 |-  ( b = x -> ( ( A i^i b ) e. E <-> ( A i^i x ) e. E ) )
31 30 elrab 
 |-  ( x e. { b e. ~P O | ( A i^i b ) e. E } <-> ( x e. ~P O /\ ( A i^i x ) e. E ) )
32 pwidg 
 |-  ( O e. V -> O e. ~P O )
33 3 32 syl 
 |-  ( ph -> O e. ~P O )
34 33 adantr 
 |-  ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) -> O e. ~P O )
35 34 elpwdifcl 
 |-  ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) -> ( O \ x ) e. ~P O )
36 2 pwldsys 
 |-  ( O e. V -> ~P O e. L )
37 3 36 syl 
 |-  ( ph -> ~P O e. L )
38 1 ispisys 
 |-  ( T e. P <-> ( T e. ~P ~P O /\ ( fi ` T ) C_ T ) )
39 5 38 sylib 
 |-  ( ph -> ( T e. ~P ~P O /\ ( fi ` T ) C_ T ) )
40 39 simpld 
 |-  ( ph -> T e. ~P ~P O )
41 40 elpwid 
 |-  ( ph -> T C_ ~P O )
42 sseq2 
 |-  ( t = ~P O -> ( T C_ t <-> T C_ ~P O ) )
43 42 intminss 
 |-  ( ( ~P O e. L /\ T C_ ~P O ) -> |^| { t e. L | T C_ t } C_ ~P O )
44 37 41 43 syl2anc 
 |-  ( ph -> |^| { t e. L | T C_ t } C_ ~P O )
45 4 44 eqsstrid 
 |-  ( ph -> E C_ ~P O )
46 45 6 sseldd 
 |-  ( ph -> A e. ~P O )
47 46 elpwid 
 |-  ( ph -> A C_ O )
48 47 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> A C_ O )
49 difin 
 |-  ( A \ ( A i^i x ) ) = ( A \ x )
50 difin2 
 |-  ( A C_ O -> ( A \ x ) = ( ( O \ x ) i^i A ) )
51 49 50 syl5eq 
 |-  ( A C_ O -> ( A \ ( A i^i x ) ) = ( ( O \ x ) i^i A ) )
52 incom 
 |-  ( ( O \ x ) i^i A ) = ( A i^i ( O \ x ) )
53 51 52 eqtrdi 
 |-  ( A C_ O -> ( A \ ( A i^i x ) ) = ( A i^i ( O \ x ) ) )
54 difuncomp 
 |-  ( A C_ O -> ( A \ ( A i^i x ) ) = ( O \ ( ( O \ A ) u. ( A i^i x ) ) ) )
55 53 54 eqtr3d 
 |-  ( A C_ O -> ( A i^i ( O \ x ) ) = ( O \ ( ( O \ A ) u. ( A i^i x ) ) ) )
56 48 55 syl 
 |-  ( ( ( ( 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 ) ) ) )
57 difeq2 
 |-  ( y = ( ( O \ A ) u. ( A i^i x ) ) -> ( O \ y ) = ( O \ ( ( O \ A ) u. ( A i^i x ) ) ) )
58 57 eleq1d 
 |-  ( y = ( ( O \ A ) u. ( A i^i x ) ) -> ( ( O \ y ) e. t <-> ( O \ ( ( O \ A ) u. ( A i^i x ) ) ) e. t ) )
59 18 simp2d 
 |-  ( t e. L -> A. x e. t ( O \ x ) e. t )
60 59 ad2antlr 
 |-  ( ( ( ( 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 )
61 difeq2 
 |-  ( x = y -> ( O \ x ) = ( O \ y ) )
62 61 eleq1d 
 |-  ( x = y -> ( ( O \ x ) e. t <-> ( O \ y ) e. t ) )
63 62 cbvralvw 
 |-  ( A. x e. t ( O \ x ) e. t <-> A. y e. t ( O \ y ) e. t )
64 60 63 sylib 
 |-  ( ( ( ( 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 )
65 simplr 
 |-  ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> t e. L )
66 6 4 eleqtrdi 
 |-  ( ph -> A e. |^| { t e. L | T C_ t } )
67 elintrabg 
 |-  ( A e. E -> ( A e. |^| { t e. L | T C_ t } <-> A. t e. L ( T C_ t -> A e. t ) ) )
68 6 67 syl 
 |-  ( ph -> ( A e. |^| { t e. L | T C_ t } <-> A. t e. L ( T C_ t -> A e. t ) ) )
69 66 68 mpbid 
 |-  ( ph -> A. t e. L ( T C_ t -> A e. t ) )
70 69 r19.21bi 
 |-  ( ( ph /\ t e. L ) -> ( T C_ t -> A e. t ) )
71 70 imp 
 |-  ( ( ( ph /\ t e. L ) /\ T C_ t ) -> A e. t )
72 71 adantllr 
 |-  ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> A e. t )
73 difeq2 
 |-  ( x = A -> ( O \ x ) = ( O \ A ) )
74 73 eleq1d 
 |-  ( x = A -> ( ( O \ x ) e. t <-> ( O \ A ) e. t ) )
75 59 adantr 
 |-  ( ( t e. L /\ A e. t ) -> A. x e. t ( O \ x ) e. t )
76 simpr 
 |-  ( ( t e. L /\ A e. t ) -> A e. t )
77 74 75 76 rspcdva 
 |-  ( ( t e. L /\ A e. t ) -> ( O \ A ) e. t )
78 65 72 77 syl2anc 
 |-  ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> ( O \ A ) e. t )
79 simpllr 
 |-  ( ( ( ( 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 ) )
80 79 simprd 
 |-  ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> ( A i^i x ) e. E )
81 80 4 eleqtrdi 
 |-  ( ( ( ( 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 } )
82 vex 
 |-  x e. _V
83 82 inex2 
 |-  ( A i^i x ) e. _V
84 elintrabg 
 |-  ( ( 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 ) ) )
85 83 84 mp1i 
 |-  ( ( ( ( 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 ) ) )
86 81 85 mpbid 
 |-  ( ( ( ( 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 ) )
87 simpr 
 |-  ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> T C_ t )
88 rspa 
 |-  ( ( 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 ) )
89 88 imp 
 |-  ( ( ( 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 86 65 87 89 syl21anc 
 |-  ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> ( A i^i x ) e. t )
91 incom 
 |-  ( ( O \ A ) i^i ( A i^i x ) ) = ( ( A i^i x ) i^i ( O \ A ) )
92 inss1 
 |-  ( A i^i x ) C_ A
93 disjdif 
 |-  ( A i^i ( O \ A ) ) = (/)
94 ssdisj 
 |-  ( ( ( A i^i x ) C_ A /\ ( A i^i ( O \ A ) ) = (/) ) -> ( ( A i^i x ) i^i ( O \ A ) ) = (/) )
95 92 93 94 mp2an 
 |-  ( ( A i^i x ) i^i ( O \ A ) ) = (/)
96 91 95 eqtri 
 |-  ( ( O \ A ) i^i ( A i^i x ) ) = (/)
97 96 a1i 
 |-  ( ( ( ( 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 ) ) = (/) )
98 2 65 78 90 97 unelldsys 
 |-  ( ( ( ( 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 )
99 58 64 98 rspcdva 
 |-  ( ( ( ( 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 )
100 56 99 eqeltrd 
 |-  ( ( ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) /\ t e. L ) /\ T C_ t ) -> ( A i^i ( O \ x ) ) e. t )
101 100 ex 
 |-  ( ( ( 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 ralrimiva 
 |-  ( ( 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 ) )
103 inex1g 
 |-  ( A e. E -> ( A i^i ( O \ x ) ) e. _V )
104 6 103 syl 
 |-  ( ph -> ( A i^i ( O \ x ) ) e. _V )
105 104 adantr 
 |-  ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) -> ( A i^i ( O \ x ) ) e. _V )
106 elintrabg 
 |-  ( ( 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 ) ) )
107 105 106 syl 
 |-  ( ( 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 ) ) )
108 102 107 mpbird 
 |-  ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) -> ( A i^i ( O \ x ) ) e. |^| { t e. L | T C_ t } )
109 108 4 eleqtrrdi 
 |-  ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) -> ( A i^i ( O \ x ) ) e. E )
110 35 109 jca 
 |-  ( ( ph /\ ( x e. ~P O /\ ( A i^i x ) e. E ) ) -> ( ( O \ x ) e. ~P O /\ ( A i^i ( O \ x ) ) e. E ) )
111 31 110 sylan2b 
 |-  ( ( 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 ) )
112 ineq2 
 |-  ( b = ( O \ x ) -> ( A i^i b ) = ( A i^i ( O \ x ) ) )
113 112 eleq1d 
 |-  ( b = ( O \ x ) -> ( ( A i^i b ) e. E <-> ( A i^i ( O \ x ) ) e. E ) )
114 113 elrab 
 |-  ( ( 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 ) )
115 111 114 sylibr 
 |-  ( ( 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 } )
116 115 ralrimiva 
 |-  ( 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 } )
117 ineq2 
 |-  ( b = U. x -> ( A i^i b ) = ( A i^i U. x ) )
118 117 eleq1d 
 |-  ( b = U. x -> ( ( A i^i b ) e. E <-> ( A i^i U. x ) e. E ) )
119 7 sspwi 
 |-  ~P { b e. ~P O | ( A i^i b ) e. E } C_ ~P ~P O
120 simplr 
 |-  ( ( ( 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 } )
121 119 120 sselid 
 |-  ( ( ( 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 )
122 121 elpwunicl 
 |-  ( ( ( 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 )
123 uniin2 
 |-  U_ y e. x ( A i^i y ) = ( A i^i U. x )
124 vex 
 |-  y e. _V
125 124 inex2 
 |-  ( A i^i y ) e. _V
126 125 dfiun3 
 |-  U_ y e. x ( A i^i y ) = U. ran ( y e. x |-> ( A i^i y ) )
127 123 126 eqtr3i 
 |-  ( A i^i U. x ) = U. ran ( y e. x |-> ( A i^i y ) )
128 simplr 
 |-  ( ( ( ( ( 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 )
129 nfv 
 |-  F/ y ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } )
130 nfv 
 |-  F/ y x ~<_ _om
131 nfdisj1 
 |-  F/ y Disj_ y e. x y
132 130 131 nfan 
 |-  F/ y ( x ~<_ _om /\ Disj_ y e. x y )
133 129 132 nfan 
 |-  F/ y ( ( ph /\ x e. ~P { b e. ~P O | ( A i^i b ) e. E } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) )
134 nfv 
 |-  F/ y t e. L
135 133 134 nfan 
 |-  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 )
136 nfv 
 |-  F/ y T C_ t
137 135 136 nfan 
 |-  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 )
138 elpwi 
 |-  ( 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 } )
139 138 ad4antlr 
 |-  ( ( ( ( ( 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 } )
140 139 sselda 
 |-  ( ( ( ( ( ( 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 } )
141 ineq2 
 |-  ( b = y -> ( A i^i b ) = ( A i^i y ) )
142 141 eleq1d 
 |-  ( b = y -> ( ( A i^i b ) e. E <-> ( A i^i y ) e. E ) )
143 142 elrab 
 |-  ( y e. { b e. ~P O | ( A i^i b ) e. E } <-> ( y e. ~P O /\ ( A i^i y ) e. E ) )
144 143 simprbi 
 |-  ( y e. { b e. ~P O | ( A i^i b ) e. E } -> ( A i^i y ) e. E )
145 140 144 syl 
 |-  ( ( ( ( ( ( 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 )
146 simpllr 
 |-  ( ( ( ( ( ( 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 )
147 simplr 
 |-  ( ( ( ( ( ( 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 )
148 4 eleq2i 
 |-  ( ( A i^i y ) e. E <-> ( A i^i y ) e. |^| { t e. L | T C_ t } )
149 125 elintrab 
 |-  ( ( A i^i y ) e. |^| { t e. L | T C_ t } <-> A. t e. L ( T C_ t -> ( A i^i y ) e. t ) )
150 148 149 bitri 
 |-  ( ( A i^i y ) e. E <-> A. t e. L ( T C_ t -> ( A i^i y ) e. t ) )
151 rspa 
 |-  ( ( 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 ) )
152 150 151 sylanb 
 |-  ( ( ( A i^i y ) e. E /\ t e. L ) -> ( T C_ t -> ( A i^i y ) e. t ) )
153 152 imp 
 |-  ( ( ( ( A i^i y ) e. E /\ t e. L ) /\ T C_ t ) -> ( A i^i y ) e. t )
154 145 146 147 153 syl21anc 
 |-  ( ( ( ( ( ( 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 )
155 154 ex 
 |-  ( ( ( ( ( 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 137 155 ralrimi 
 |-  ( ( ( ( ( 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 )
157 eqid 
 |-  ( y e. x |-> ( A i^i y ) ) = ( y e. x |-> ( A i^i y ) )
158 157 rnmptss 
 |-  ( A. y e. x ( A i^i y ) e. t -> ran ( y e. x |-> ( A i^i y ) ) C_ t )
159 156 158 syl 
 |-  ( ( ( ( ( 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 )
160 128 159 sselpwd 
 |-  ( ( ( ( ( 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 )
161 simpllr 
 |-  ( ( ( ( ( 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 ) )
162 161 simpld 
 |-  ( ( ( ( ( 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 )
163 1stcrestlem 
 |-  ( x ~<_ _om -> ran ( y e. x |-> ( A i^i y ) ) ~<_ _om )
164 162 163 syl 
 |-  ( ( ( ( ( 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 )
165 161 simprd 
 |-  ( ( ( ( ( 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 )
166 disjin2 
 |-  ( Disj_ y e. x y -> Disj_ y e. x ( A i^i y ) )
167 disjrnmpt 
 |-  ( Disj_ y e. x ( A i^i y ) -> Disj_ z e. ran ( y e. x |-> ( A i^i y ) ) z )
168 165 166 167 3syl 
 |-  ( ( ( ( ( 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 )
169 nfmpt1 
 |-  F/_ y ( y e. x |-> ( A i^i y ) )
170 169 nfrn 
 |-  F/_ y ran ( y e. x |-> ( A i^i y ) )
171 nfcv 
 |-  F/_ z y
172 nfcv 
 |-  F/_ y z
173 id 
 |-  ( y = z -> y = z )
174 170 171 172 173 cbvdisjf 
 |-  ( Disj_ y e. ran ( y e. x |-> ( A i^i y ) ) y <-> Disj_ z e. ran ( y e. x |-> ( A i^i y ) ) z )
175 168 174 sylibr 
 |-  ( ( ( ( ( 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 )
176 breq1 
 |-  ( z = ran ( y e. x |-> ( A i^i y ) ) -> ( z ~<_ _om <-> ran ( y e. x |-> ( A i^i y ) ) ~<_ _om ) )
177 172 170 disjeq1f 
 |-  ( 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 ) )
178 176 177 anbi12d 
 |-  ( 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 ) ) )
179 unieq 
 |-  ( z = ran ( y e. x |-> ( A i^i y ) ) -> U. z = U. ran ( y e. x |-> ( A i^i y ) ) )
180 179 eleq1d 
 |-  ( z = ran ( y e. x |-> ( A i^i y ) ) -> ( U. z e. t <-> U. ran ( y e. x |-> ( A i^i y ) ) e. t ) )
181 178 180 imbi12d 
 |-  ( 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 ) ) )
182 18 simp3d 
 |-  ( t e. L -> A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) )
183 breq1 
 |-  ( x = z -> ( x ~<_ _om <-> z ~<_ _om ) )
184 disjeq1 
 |-  ( x = z -> ( Disj_ y e. x y <-> Disj_ y e. z y ) )
185 183 184 anbi12d 
 |-  ( x = z -> ( ( x ~<_ _om /\ Disj_ y e. x y ) <-> ( z ~<_ _om /\ Disj_ y e. z y ) ) )
186 unieq 
 |-  ( x = z -> U. x = U. z )
187 186 eleq1d 
 |-  ( x = z -> ( U. x e. t <-> U. z e. t ) )
188 185 187 imbi12d 
 |-  ( x = z -> ( ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) <-> ( ( z ~<_ _om /\ Disj_ y e. z y ) -> U. z e. t ) ) )
189 188 cbvralvw 
 |-  ( 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 ) )
190 182 189 sylib 
 |-  ( t e. L -> A. z e. ~P t ( ( z ~<_ _om /\ Disj_ y e. z y ) -> U. z e. t ) )
191 190 adantr 
 |-  ( ( 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 ) )
192 simpr 
 |-  ( ( 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 )
193 181 191 192 rspcdva 
 |-  ( ( 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 ) )
194 193 imp 
 |-  ( ( ( 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 128 160 164 175 194 syl22anc 
 |-  ( ( ( ( ( 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 )
196 127 195 eqeltrid 
 |-  ( ( ( ( ( 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 )
197 196 ex 
 |-  ( ( ( ( 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 ralrimiva 
 |-  ( ( ( 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 ) )
199 vuniex 
 |-  U. x e. _V
200 199 inex2 
 |-  ( A i^i U. x ) e. _V
201 200 elintrab 
 |-  ( ( 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 ) )
202 198 201 sylibr 
 |-  ( ( ( 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 } )
203 202 4 eleqtrrdi 
 |-  ( ( ( 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 )
204 118 122 203 elrabd 
 |-  ( ( ( 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 } )
205 204 ex 
 |-  ( ( 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 } ) )
206 205 ralrimiva 
 |-  ( 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 } ) )
207 28 116 206 3jca 
 |-  ( 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 } ) ) )
208 2 isldsys 
 |-  ( { 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 } ) ) ) )
209 12 207 208 sylanbrc 
 |-  ( ph -> { b e. ~P O | ( A i^i b ) e. E } e. L )