Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ldgenpisyslem1 Structured version   Visualization version   Unicode version

Theorem ldgenpisyslem1 28985
Description: Lemma for ldgenpisys 28988. (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.
StepHypRef Expression
1 ssrab2 3514 . . . 4  |-  { b  e.  ~P O  | 
( A  i^i  b
)  e.  E }  C_ 
~P O
2 dynkin.o . . . . 5  |-  ( ph  ->  O  e.  V )
3 pwexg 4587 . . . . 5  |-  ( O  e.  V  ->  ~P O  e.  _V )
4 rabexg 4553 . . . . 5  |-  ( ~P O  e.  _V  ->  { b  e.  ~P O  |  ( A  i^i  b )  e.  E }  e.  _V )
5 elpwg 3959 . . . . 5  |-  ( { 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 ) )
62, 3, 4, 54syl 19 . . . 4  |-  ( 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 ) )
71, 6mpbiri 237 . . 3  |-  ( ph  ->  { b  e.  ~P O  |  ( A  i^i  b )  e.  E }  e.  ~P ~P O )
8 0elpw 4572 . . . . . . 7  |-  (/)  e.  ~P O
98a1i 11 . . . . . 6  |-  ( ph  -> 
(/)  e.  ~P O
)
10 in0 3760 . . . . . . . 8  |-  ( A  i^i  (/) )  =  (/)
11 dynkin.l . . . . . . . . . . . . . . 15  |-  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
) ) }
1211isldsys 28978 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) )
1312simprbi 466 . . . . . . . . . . . . 13  |-  ( 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
) ) )
1413simp1d 1020 . . . . . . . . . . . 12  |-  ( t  e.  L  ->  (/)  e.  t )
1514ad2antlr 733 . . . . . . . . . . 11  |-  ( ( ( ph  /\  t  e.  L )  /\  T  C_  t )  ->  (/)  e.  t )
1615ex 436 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  L )  ->  ( T  C_  t  ->  (/)  e.  t ) )
1716ralrimiva 2802 . . . . . . . . 9  |-  ( ph  ->  A. t  e.  L  ( T  C_  t  ->  (/) 
e.  t ) )
188elexi 3055 . . . . . . . . . 10  |-  (/)  e.  _V
1918elintrab 4246 . . . . . . . . 9  |-  ( (/)  e.  |^| { t  e.  L  |  T  C_  t }  <->  A. t  e.  L  ( T  C_  t  ->  (/) 
e.  t ) )
2017, 19sylibr 216 . . . . . . . 8  |-  ( ph  -> 
(/)  e.  |^| { t  e.  L  |  T  C_  t } )
2110, 20syl5eqel 2533 . . . . . . 7  |-  ( ph  ->  ( A  i^i  (/) )  e. 
|^| { t  e.  L  |  T  C_  t } )
22 ldgenpisys.e . . . . . . 7  |-  E  = 
|^| { t  e.  L  |  T  C_  t }
2321, 22syl6eleqr 2540 . . . . . 6  |-  ( ph  ->  ( A  i^i  (/) )  e.  E )
249, 23jca 535 . . . . 5  |-  ( ph  ->  ( (/)  e.  ~P O  /\  ( A  i^i  (/) )  e.  E ) )
25 ineq2 3628 . . . . . . 7  |-  ( b  =  (/)  ->  ( A  i^i  b )  =  ( A  i^i  (/) ) )
2625eleq1d 2513 . . . . . 6  |-  ( b  =  (/)  ->  ( ( A  i^i  b )  e.  E  <->  ( A  i^i  (/) )  e.  E
) )
2726elrab 3196 . . . . 5  |-  ( (/)  e.  { b  e.  ~P O  |  ( A  i^i  b )  e.  E } 
<->  ( (/)  e.  ~P O  /\  ( A  i^i  (/) )  e.  E ) )
2824, 27sylibr 216 . . . 4  |-  ( ph  -> 
(/)  e.  { b  e.  ~P O  |  ( A  i^i  b )  e.  E } )
29 ineq2 3628 . . . . . . . . 9  |-  ( b  =  x  ->  ( A  i^i  b )  =  ( A  i^i  x
) )
3029eleq1d 2513 . . . . . . . 8  |-  ( b  =  x  ->  (
( A  i^i  b
)  e.  E  <->  ( A  i^i  x )  e.  E
) )
3130elrab 3196 . . . . . . 7  |-  ( x  e.  { b  e. 
~P O  |  ( A  i^i  b )  e.  E }  <->  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E ) )
32 pwidg 3964 . . . . . . . . . . 11  |-  ( O  e.  V  ->  O  e.  ~P O )
332, 32syl 17 . . . . . . . . . 10  |-  ( ph  ->  O  e.  ~P O
)
3433adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E ) )  ->  O  e.  ~P O
)
3534elpwdifcl 28155 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E ) )  -> 
( O  \  x
)  e.  ~P O
)
3611pwldsys 28979 . . . . . . . . . . . . . . . . . . . 20  |-  ( O  e.  V  ->  ~P O  e.  L )
372, 36syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ~P O  e.  L
)
38 ldgenpisys.1 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  T  e.  P )
39 dynkin.p . . . . . . . . . . . . . . . . . . . . . . 23  |-  P  =  { s  e.  ~P ~P O  |  ( fi `  s )  C_  s }
4039ispisys 28974 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T  e.  P  <->  ( T  e.  ~P ~P O  /\  ( fi `  T ) 
C_  T ) )
4138, 40sylib 200 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( T  e.  ~P ~P O  /\  ( fi `  T )  C_  T ) )
4241simpld 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  T  e.  ~P ~P O )
43 elpwi 3960 . . . . . . . . . . . . . . . . . . . 20  |-  ( T  e.  ~P ~P O  ->  T  C_  ~P O
)
4442, 43syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  T  C_  ~P O
)
45 sseq2 3454 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  ~P O  -> 
( T  C_  t  <->  T 
C_  ~P O ) )
4645intminss 4261 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ~P O  e.  L  /\  T  C_  ~P O
)  ->  |^| { t  e.  L  |  T  C_  t }  C_  ~P O )
4737, 44, 46syl2anc 667 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  |^| { t  e.  L  |  T  C_  t }  C_  ~P O
)
4822, 47syl5eqss 3476 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  E  C_  ~P O
)
49 ldgenpisyslem1.1 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A  e.  E )
5048, 49sseldd 3433 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A  e.  ~P O
)
51 elpwi 3960 . . . . . . . . . . . . . . . 16  |-  ( A  e.  ~P O  ->  A  C_  O )
5250, 51syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  C_  O )
5352ad3antrrr 736 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E
) )  /\  t  e.  L )  /\  T  C_  t )  ->  A  C_  O )
54 difin 3680 . . . . . . . . . . . . . . . . . 18  |-  ( A 
\  ( A  i^i  x ) )  =  ( A  \  x
)
5554a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( A 
C_  O  ->  ( A  \  ( A  i^i  x ) )  =  ( A  \  x
) )
56 difin2 3705 . . . . . . . . . . . . . . . . 17  |-  ( A 
C_  O  ->  ( A  \  x )  =  ( ( O  \  x )  i^i  A
) )
5755, 56eqtrd 2485 . . . . . . . . . . . . . . . 16  |-  ( A 
C_  O  ->  ( A  \  ( A  i^i  x ) )  =  ( ( O  \  x )  i^i  A
) )
58 incom 3625 . . . . . . . . . . . . . . . 16  |-  ( ( O  \  x )  i^i  A )  =  ( A  i^i  ( O  \  x ) )
5957, 58syl6eq 2501 . . . . . . . . . . . . . . 15  |-  ( A 
C_  O  ->  ( A  \  ( A  i^i  x ) )  =  ( A  i^i  ( O  \  x ) ) )
60 difuncomp 28166 . . . . . . . . . . . . . . 15  |-  ( A 
C_  O  ->  ( A  \  ( A  i^i  x ) )  =  ( O  \  (
( O  \  A
)  u.  ( A  i^i  x ) ) ) )
6159, 60eqtr3d 2487 . . . . . . . . . . . . . 14  |-  ( A 
C_  O  ->  ( A  i^i  ( O  \  x ) )  =  ( O  \  (
( O  \  A
)  u.  ( A  i^i  x ) ) ) )
6253, 61syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) ) ) )
63 difeq2 3545 . . . . . . . . . . . . . . 15  |-  ( y  =  ( ( O 
\  A )  u.  ( A  i^i  x
) )  ->  ( O  \  y )  =  ( O  \  (
( O  \  A
)  u.  ( A  i^i  x ) ) ) )
6463eleq1d 2513 . . . . . . . . . . . . . 14  |-  ( y  =  ( ( O 
\  A )  u.  ( A  i^i  x
) )  ->  (
( O  \  y
)  e.  t  <->  ( O  \  ( ( O  \  A )  u.  ( A  i^i  x ) ) )  e.  t ) )
65 simplr 762 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E
) )  /\  t  e.  L )  /\  T  C_  t )  ->  t  e.  L )
6613simp2d 1021 . . . . . . . . . . . . . . . 16  |-  ( t  e.  L  ->  A. x  e.  t  ( O  \  x )  e.  t )
6765, 66syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 )
68 difeq2 3545 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  ( O  \  x )  =  ( O  \  y
) )
6968eleq1d 2513 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
( O  \  x
)  e.  t  <->  ( O  \  y )  e.  t ) )
7069cbvralv 3019 . . . . . . . . . . . . . . 15  |-  ( A. x  e.  t  ( O  \  x )  e.  t  <->  A. y  e.  t  ( O  \  y
)  e.  t )
7167, 70sylib 200 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
7249, 22syl6eleq 2539 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A  e.  |^| { t  e.  L  |  T  C_  t } )
73 elintrabg 4247 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A  e.  E  ->  ( A  e.  |^| { t  e.  L  |  T  C_  t }  <->  A. t  e.  L  ( T  C_  t  ->  A  e.  t ) ) )
7449, 73syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( A  e.  |^| { t  e.  L  |  T  C_  t }  <->  A. t  e.  L  ( T  C_  t  ->  A  e.  t ) ) )
7572, 74mpbid 214 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. t  e.  L  ( T  C_  t  ->  A  e.  t )
)
7675r19.21bi 2757 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  L )  ->  ( T  C_  t  ->  A  e.  t ) )
7776imp 431 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  t  e.  L )  /\  T  C_  t )  ->  A  e.  t )
7877adantllr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E
) )  /\  t  e.  L )  /\  T  C_  t )  ->  A  e.  t )
79 difeq2 3545 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  A  ->  ( O  \  x )  =  ( O  \  A
) )
8079eleq1d 2513 . . . . . . . . . . . . . . . . 17  |-  ( x  =  A  ->  (
( O  \  x
)  e.  t  <->  ( O  \  A )  e.  t ) )
8166adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( ( t  e.  L  /\  A  e.  t )  ->  A. x  e.  t  ( O  \  x
)  e.  t )
82 simpr 463 . . . . . . . . . . . . . . . . 17  |-  ( ( t  e.  L  /\  A  e.  t )  ->  A  e.  t )
8380, 81, 82rspcdva 28115 . . . . . . . . . . . . . . . 16  |-  ( ( t  e.  L  /\  A  e.  t )  ->  ( O  \  A
)  e.  t )
8465, 78, 83syl2anc 667 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E
) )  /\  t  e.  L )  /\  T  C_  t )  ->  ( O  \  A )  e.  t )
85 simpllr 769 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 ) )
8685simprd 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E
) )  /\  t  e.  L )  /\  T  C_  t )  ->  ( A  i^i  x )  e.  E )
8786, 22syl6eleq 2539 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 } )
88 vex 3048 . . . . . . . . . . . . . . . . . . . 20  |-  x  e. 
_V
8988inex2 4545 . . . . . . . . . . . . . . . . . . 19  |-  ( A  i^i  x )  e. 
_V
9089a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E
) )  /\  t  e.  L )  /\  T  C_  t )  ->  ( A  i^i  x )  e. 
_V )
91 elintrabg 4247 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) )
9290, 91syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) ) )
9387, 92mpbid 214 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) )
94 simpr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E
) )  /\  t  e.  L )  /\  T  C_  t )  ->  T  C_  t )
95 rspa 2755 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 ) )
9695imp 431 . . . . . . . . . . . . . . . 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 )
9793, 65, 94, 96syl21anc 1267 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E
) )  /\  t  e.  L )  /\  T  C_  t )  ->  ( A  i^i  x )  e.  t )
98 incom 3625 . . . . . . . . . . . . . . . . 17  |-  ( ( O  \  A )  i^i  ( A  i^i  x ) )  =  ( ( A  i^i  x )  i^i  ( O  \  A ) )
99 inss1 3652 . . . . . . . . . . . . . . . . . 18  |-  ( A  i^i  x )  C_  A
100 disjdif 3839 . . . . . . . . . . . . . . . . . 18  |-  ( A  i^i  ( O  \  A ) )  =  (/)
101 ssdisj 3814 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  i^i  x
)  C_  A  /\  ( A  i^i  ( O  \  A ) )  =  (/) )  ->  (
( A  i^i  x
)  i^i  ( O  \  A ) )  =  (/) )
10299, 100, 101mp2an 678 . . . . . . . . . . . . . . . . 17  |-  ( ( A  i^i  x )  i^i  ( O  \  A ) )  =  (/)
10398, 102eqtri 2473 . . . . . . . . . . . . . . . 16  |-  ( ( O  \  A )  i^i  ( A  i^i  x ) )  =  (/)
104103a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) )  =  (/) )
10511, 65, 84, 97, 104unelldsys 28980 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 )
10664, 71, 105rspcdva 28115 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 )
10762, 106eqeltrd 2529 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E
) )  /\  t  e.  L )  /\  T  C_  t )  ->  ( A  i^i  ( O  \  x ) )  e.  t )
108107ex 436 . . . . . . . . . . 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 ) )
109108ralrimiva 2802 . . . . . . . . . 10  |-  ( (
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 ) )
110 inex1g 4546 . . . . . . . . . . . . 13  |-  ( A  e.  E  ->  ( A  i^i  ( O  \  x ) )  e. 
_V )
11149, 110syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  i^i  ( O  \  x ) )  e.  _V )
112111adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E ) )  -> 
( A  i^i  ( O  \  x ) )  e.  _V )
113 elintrabg 4247 . . . . . . . . . . 11  |-  ( ( 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 ) ) )
114112, 113syl 17 . . . . . . . . . 10  |-  ( (
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 ) ) )
115109, 114mpbird 236 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E ) )  -> 
( A  i^i  ( O  \  x ) )  e.  |^| { t  e.  L  |  T  C_  t } )
116115, 22syl6eleqr 2540 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E ) )  -> 
( A  i^i  ( O  \  x ) )  e.  E )
11735, 116jca 535 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ~P O  /\  ( A  i^i  x )  e.  E ) )  -> 
( ( O  \  x )  e.  ~P O  /\  ( A  i^i  ( O  \  x
) )  e.  E
) )
11831, 117sylan2b 478 . . . . . 6  |-  ( (
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 ) )
119 ineq2 3628 . . . . . . . 8  |-  ( b  =  ( O  \  x )  ->  ( A  i^i  b )  =  ( A  i^i  ( O  \  x ) ) )
120119eleq1d 2513 . . . . . . 7  |-  ( b  =  ( O  \  x )  ->  (
( A  i^i  b
)  e.  E  <->  ( A  i^i  ( O  \  x
) )  e.  E
) )
121120elrab 3196 . . . . . 6  |-  ( ( 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 ) )
122118, 121sylibr 216 . . . . 5  |-  ( (
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 } )
123122ralrimiva 2802 . . . 4  |-  ( 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 } )
1242ad2antrr 732 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ~P { b  e. 
~P O  |  ( A  i^i  b )  e.  E } )  /\  ( x  ~<_  om 
/\ Disj  y  e.  x  y ) )  ->  O  e.  V )
125 sspwb 4649 . . . . . . . . . . 11  |-  ( { 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 )
1261, 125mpbi 212 . . . . . . . . . 10  |-  ~P {
b  e.  ~P O  |  ( A  i^i  b )  e.  E }  C_  ~P ~P O
127 simplr 762 . . . . . . . . . 10  |-  ( ( ( 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 } )
128126, 127sseldi 3430 . . . . . . . . 9  |-  ( ( ( 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 )
129124, 128elpwunicl 28168 . . . . . . . 8  |-  ( ( ( 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 )
130 uniin2 28165 . . . . . . . . . . . . . 14  |-  U_ y  e.  x  ( A  i^i  y )  =  ( A  i^i  U. x
)
131 vex 3048 . . . . . . . . . . . . . . . 16  |-  y  e. 
_V
132131inex2 4545 . . . . . . . . . . . . . . 15  |-  ( A  i^i  y )  e. 
_V
133132dfiun3 5089 . . . . . . . . . . . . . 14  |-  U_ y  e.  x  ( A  i^i  y )  =  U. ran  ( y  e.  x  |->  ( A  i^i  y
) )
134130, 133eqtr3i 2475 . . . . . . . . . . . . 13  |-  ( A  i^i  U. x )  =  U. ran  (
y  e.  x  |->  ( A  i^i  y ) )
135 simplr 762 . . . . . . . . . . . . . 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
)  ->  t  e.  L )
136 nfv 1761 . . . . . . . . . . . . . . . . . . . 20  |-  F/ y ( ph  /\  x  e.  ~P { b  e. 
~P O  |  ( A  i^i  b )  e.  E } )
137 nfv 1761 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ y  x  ~<_  om
138 nfdisj1 4386 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ yDisj  y  e.  x  y
139137, 138nfan 2011 . . . . . . . . . . . . . . . . . . . 20  |-  F/ y ( x  ~<_  om  /\ Disj  y  e.  x  y )
140136, 139nfan 2011 . . . . . . . . . . . . . . . . . . 19  |-  F/ y ( ( ph  /\  x  e.  ~P { b  e.  ~P O  | 
( A  i^i  b
)  e.  E }
)  /\  ( x  ~<_  om  /\ Disj  y  e.  x  y ) )
141 nfv 1761 . . . . . . . . . . . . . . . . . . 19  |-  F/ y  t  e.  L
142140, 141nfan 2011 . . . . . . . . . . . . . . . . . 18  |-  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
)
143 nfv 1761 . . . . . . . . . . . . . . . . . 18  |-  F/ y  T  C_  t
144142, 143nfan 2011 . . . . . . . . . . . . . . . . 17  |-  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
)
145 elpwi 3960 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 } )
146145ad4antlr 739 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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 }
)
147146sselda 3432 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
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 } )
148 ineq2 3628 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  =  y  ->  ( A  i^i  b )  =  ( A  i^i  y
) )
149148eleq1d 2513 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( b  =  y  ->  (
( A  i^i  b
)  e.  E  <->  ( A  i^i  y )  e.  E
) )
150149elrab 3196 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  { b  e. 
~P O  |  ( A  i^i  b )  e.  E }  <->  ( y  e.  ~P O  /\  ( A  i^i  y )  e.  E ) )
151150simprbi 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  { b  e. 
~P O  |  ( A  i^i  b )  e.  E }  ->  ( A  i^i  y )  e.  E )
152147, 151syl 17 . . . . . . . . . . . . . . . . . . 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
)  /\  y  e.  x )  ->  ( A  i^i  y )  e.  E )
153135adantr 467 . . . . . . . . . . . . . . . . . . 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
)  /\  y  e.  x )  ->  t  e.  L )
154 simplr 762 . . . . . . . . . . . . . . . . . . 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
)  /\  y  e.  x )  ->  T  C_  t )
15522eleq2i 2521 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  i^i  y )  e.  E  <->  ( A  i^i  y )  e.  |^| { t  e.  L  |  T  C_  t } )
156132elintrab 4246 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( A  i^i  y )  e.  |^| { t  e.  L  |  T  C_  t }  <->  A. t  e.  L  ( T  C_  t  -> 
( A  i^i  y
)  e.  t ) )
157155, 156bitri 253 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  i^i  y )  e.  E  <->  A. t  e.  L  ( T  C_  t  ->  ( A  i^i  y )  e.  t ) )
158 rspa 2755 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 ) )
159157, 158sylanb 475 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A  i^i  y
)  e.  E  /\  t  e.  L )  ->  ( T  C_  t  ->  ( A  i^i  y
)  e.  t ) )
160159imp 431 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  i^i  y )  e.  E  /\  t  e.  L
)  /\  T  C_  t
)  ->  ( A  i^i  y )  e.  t )
161152, 153, 154, 160syl21anc 1267 . . . . . . . . . . . . . . . . . 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 )  ->  ( A  i^i  y )  e.  t )
162161ex 436 . . . . . . . . . . . . . . . . 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.  t ) )
163144, 162ralrimi 2788 . . . . . . . . . . . . . . . 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
)  ->  A. y  e.  x  ( A  i^i  y )  e.  t )
164 eqid 2451 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  x  |->  ( A  i^i  y ) )  =  ( y  e.  x  |->  ( A  i^i  y ) )
165164rnmptss 6052 . . . . . . . . . . . . . . . 16  |-  ( A. y  e.  x  ( A  i^i  y )  e.  t  ->  ran  ( y  e.  x  |->  ( A  i^i  y ) ) 
C_  t )
166163, 165syl 17 . . . . . . . . . . . . . . 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
)  ->  ran  ( y  e.  x  |->  ( A  i^i  y ) ) 
C_  t )
167135, 166sselpwd 28153 . . . . . . . . . . . . . 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
)  ->  ran  ( y  e.  x  |->  ( A  i^i  y ) )  e.  ~P t )
168 simpllr 769 . . . . . . . . . . . . . . . 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
)  ->  ( x  ~<_  om  /\ Disj  y  e.  x  y ) )
169168simpld 461 . . . . . . . . . . . . . . 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
)  ->  x  ~<_  om )
170 mptct 28302 . . . . . . . . . . . . . . . 16  |-  ( x  ~<_  om  ->  ( y  e.  x  |->  ( A  i^i  y ) )  ~<_  om )
171 rnct 28300 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  x  |->  ( A  i^i  y ) )  ~<_  om  ->  ran  (
y  e.  x  |->  ( A  i^i  y ) )  ~<_  om )
172170, 171syl 17 . . . . . . . . . . . . . . 15  |-  ( x  ~<_  om  ->  ran  ( y  e.  x  |->  ( A  i^i  y ) )  ~<_  om )
173169, 172syl 17 . . . . . . . . . . . . . 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
)  ->  ran  ( y  e.  x  |->  ( A  i^i  y ) )  ~<_  om )
174168simprd 465 . . . . . . . . . . . . . . . 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
)  -> Disj  y  e.  x  y )
175 disjin2 28197 . . . . . . . . . . . . . . . 16  |-  (Disj  y  e.  x  y  -> Disj  y  e.  x  ( A  i^i  y ) )
176 disjrnmpt 28195 . . . . . . . . . . . . . . . 16  |-  (Disj  y  e.  x  ( A  i^i  y )  -> Disj  z  e. 
ran  ( y  e.  x  |->  ( A  i^i  y ) ) z )
177174, 175, 1763syl 18 . . . . . . . . . . . . . . 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
)  -> Disj  z  e.  ran  ( y  e.  x  |->  ( A  i^i  y
) ) z )
178 nfmpt1 4492 . . . . . . . . . . . . . . . . 17  |-  F/_ y
( y  e.  x  |->  ( A  i^i  y
) )
179178nfrn 5077 . . . . . . . . . . . . . . . 16  |-  F/_ y ran  ( y  e.  x  |->  ( A  i^i  y
) )
180 nfcv 2592 . . . . . . . . . . . . . . . 16  |-  F/_ z
y
181 nfcv 2592 . . . . . . . . . . . . . . . 16  |-  F/_ y
z
182 id 22 . . . . . . . . . . . . . . . 16  |-  ( y  =  z  ->  y  =  z )
183179, 180, 181, 182cbvdisjf 28182 . . . . . . . . . . . . . . 15  |-  (Disj  y  e.  ran  ( y  e.  x  |->  ( A  i^i  y ) ) y  <-> Disj  z  e.  ran  ( y  e.  x  |->  ( A  i^i  y ) ) z )
184177, 183sylibr 216 . . . . . . . . . . . . . 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.  ran  ( y  e.  x  |->  ( A  i^i  y
) ) y )
185 breq1 4405 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ran  ( y  e.  x  |->  ( A  i^i  y ) )  ->  ( z  ~<_  om  <->  ran  ( y  e.  x  |->  ( A  i^i  y
) )  ~<_  om )
)
186181, 179disjeq1f 28184 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) )
187185, 186anbi12d 717 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) )
188 unieq 4206 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ran  ( y  e.  x  |->  ( A  i^i  y ) )  ->  U. z  =  U. ran  ( y  e.  x  |->  ( A  i^i  y
) ) )
189188eleq1d 2513 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ran  ( y  e.  x  |->  ( A  i^i  y ) )  ->  ( U. z  e.  t  <->  U. ran  ( y  e.  x  |->  ( A  i^i  y ) )  e.  t ) )
190187, 189imbi12d 322 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) )
19113simp3d 1022 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  L  ->  A. x  e.  ~P  t ( ( x  ~<_  om  /\ Disj  y  e.  x  y )  ->  U. x  e.  t
) )
192 breq1 4405 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (
x  ~<_  om  <->  z  ~<_  om )
)
193 disjeq1 4380 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  (Disj  y  e.  x  y  <-> Disj  y  e.  z  y ) )
194192, 193anbi12d 717 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  (
( x  ~<_  om  /\ Disj  y  e.  x  y )  <-> 
( z  ~<_  om  /\ Disj  y  e.  z  y ) ) )
195 unieq 4206 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  z  ->  U. x  =  U. z )
196195eleq1d 2513 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  z  ->  ( U. x  e.  t  <->  U. z  e.  t ) )
197194, 196imbi12d 322 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  z  ->  (
( ( x  ~<_  om 
/\ Disj  y  e.  x  y )  ->  U. x  e.  t )  <->  ( (
z  ~<_  om  /\ Disj  y  e.  z  y )  ->  U. z  e.  t
) ) )
198197cbvralv 3019 . . . . . . . . . . . . . . . . . 18  |-  ( 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
) )
199191, 198sylib 200 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  L  ->  A. z  e.  ~P  t ( ( z  ~<_  om  /\ Disj  y  e.  z  y )  ->  U. z  e.  t
) )
200199adantr 467 . . . . . . . . . . . . . . . 16  |-  ( ( 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
) )
201 simpr 463 . . . . . . . . . . . . . . . 16  |-  ( ( 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 )
202190, 200, 201rspcdva 28115 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) )
203202imp 431 . . . . . . . . . . . . . 14  |-  ( ( ( 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 )
204135, 167, 173, 184, 203syl22anc 1269 . . . . . . . . . . . . 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
)  ->  U. ran  (
y  e.  x  |->  ( A  i^i  y ) )  e.  t )
205134, 204syl5eqel 2533 . . . . . . . . . . . 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
)  ->  ( A  i^i  U. x )  e.  t )
206205ex 436 . . . . . . . . . . 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  ->  ( A  i^i  U. x )  e.  t ) )
207206ralrimiva 2802 . . . . . . . . . 10  |-  ( ( ( 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 ) )
20888uniex 6587 . . . . . . . . . . . 12  |-  U. x  e.  _V
209208inex2 4545 . . . . . . . . . . 11  |-  ( A  i^i  U. x )  e.  _V
210209elintrab 4246 . . . . . . . . . 10  |-  ( ( 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 ) )
211207, 210sylibr 216 . . . . . . . . 9  |-  ( ( ( 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 } )
212211, 22syl6eleqr 2540 . . . . . . . 8  |-  ( ( ( 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 )
213129, 212jca 535 . . . . . . 7  |-  ( ( ( 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  /\  ( A  i^i  U. x )  e.  E
) )
214 ineq2 3628 . . . . . . . . 9  |-  ( b  =  U. x  -> 
( A  i^i  b
)  =  ( A  i^i  U. x ) )
215214eleq1d 2513 . . . . . . . 8  |-  ( b  =  U. x  -> 
( ( A  i^i  b )  e.  E  <->  ( A  i^i  U. x
)  e.  E ) )
216215elrab 3196 . . . . . . 7  |-  ( 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
) )
217213, 216sylibr 216 . . . . . 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.  { b  e.  ~P O  |  ( A  i^i  b )  e.  E } )
218217ex 436 . . . . 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 } ) )
219218ralrimiva 2802 . . . 4  |-  ( 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 } ) )
22028, 123, 2193jca 1188 . . 3  |-  ( 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 } ) ) )
2217, 220jca 535 . 2  |-  ( ph  ->  ( { 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 } ) ) ) )
22211isldsys 28978 . 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 } ) ) ) )
223221, 222sylibr 216 1  |-  ( ph  ->  { b  e.  ~P O  |  ( A  i^i  b )  e.  E }  e.  L )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 985    = wceq 1444    e. wcel 1887   A.wral 2737   {crab 2741   _Vcvv 3045    \ cdif 3401    u. cun 3402    i^i cin 3403    C_ wss 3404   (/)c0 3731   ~Pcpw 3951   U.cuni 4198   |^|cint 4234   U_ciun 4278  Disj wdisj 4373   class class class wbr 4402    |-> cmpt 4461   ran crn 4835   ` cfv 5582   omcom 6692    ~<_ cdom 7567   ficfi 7924
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-inf2 8146  ax-ac2 8893
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-disj 4374  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-se 4794  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-isom 5591  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-om 6693  df-1st 6793  df-2nd 6794  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-2o 7183  df-oadd 7186  df-er 7363  df-map 7474  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-oi 8025  df-card 8373  df-acn 8376  df-ac 8547  df-cda 8598
This theorem is referenced by:  ldgenpisyslem2  28986
  Copyright terms: Public domain W3C validator