This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfon2lem7

Description: Lemma for dfon2 . All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011)

Ref Expression
Hypothesis dfon2lem7.1 
|- A e. _V
Assertion dfon2lem7 
|- ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( B e. A -> A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) )

Proof

Step Hyp Ref Expression
1 dfon2lem7.1 
 |-  A e. _V
2 elequ1 
 |-  ( t = z -> ( t e. t <-> z e. t ) )
3 elequ2 
 |-  ( t = z -> ( z e. t <-> z e. z ) )
4 2 3 bitrd 
 |-  ( t = z -> ( t e. t <-> z e. z ) )
5 4 notbid 
 |-  ( t = z -> ( -. t e. t <-> -. z e. z ) )
6 5 cbvralvw 
 |-  ( A. t e. x -. t e. t <-> A. z e. x -. z e. z )
7 6 biimpi 
 |-  ( A. t e. x -. t e. t -> A. z e. x -. z e. z )
8 7 ralimi 
 |-  ( A. x e. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } A. t e. x -. t e. t -> A. x e. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } A. z e. x -. z e. z )
9 untuni 
 |-  ( A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -. z e. z <-> A. x e. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } A. z e. x -. z e. z )
10 8 9 sylibr 
 |-  ( A. x e. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } A. t e. x -. t e. t -> A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -. z e. z )
11 vex 
 |-  x e. _V
12 sseq1 
 |-  ( w = x -> ( w C_ A <-> x C_ A ) )
13 treq 
 |-  ( w = x -> ( Tr w <-> Tr x ) )
14 raleq 
 |-  ( w = x -> ( A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) <-> A. t e. x A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) )
15 12 13 14 3anbi123d 
 |-  ( w = x -> ( ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) <-> ( x C_ A /\ Tr x /\ A. t e. x A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) ) )
16 11 15 elab 
 |-  ( x e. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } <-> ( x C_ A /\ Tr x /\ A. t e. x A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) )
17 vex 
 |-  t e. _V
18 dfon2lem3 
 |-  ( t e. _V -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( Tr t /\ A. u e. t -. u e. u ) ) )
19 17 18 ax-mp 
 |-  ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( Tr t /\ A. u e. t -. u e. u ) )
20 19 simprd 
 |-  ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> A. u e. t -. u e. u )
21 untelirr 
 |-  ( A. u e. t -. u e. u -> -. t e. t )
22 20 21 syl 
 |-  ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> -. t e. t )
23 22 ralimi 
 |-  ( A. t e. x A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> A. t e. x -. t e. t )
24 23 3ad2ant3 
 |-  ( ( x C_ A /\ Tr x /\ A. t e. x A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) -> A. t e. x -. t e. t )
25 16 24 sylbi 
 |-  ( x e. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> A. t e. x -. t e. t )
26 10 25 mprg 
 |-  A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -. z e. z
27 untelirr 
 |-  ( A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -. z e. z -> -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } )
28 psseq2 
 |-  ( t = u -> ( y C. t <-> y C. u ) )
29 28 anbi1d 
 |-  ( t = u -> ( ( y C. t /\ Tr y ) <-> ( y C. u /\ Tr y ) ) )
30 elequ2 
 |-  ( t = u -> ( y e. t <-> y e. u ) )
31 29 30 imbi12d 
 |-  ( t = u -> ( ( ( y C. t /\ Tr y ) -> y e. t ) <-> ( ( y C. u /\ Tr y ) -> y e. u ) ) )
32 31 albidv 
 |-  ( t = u -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) <-> A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) )
33 32 cbvralvw 
 |-  ( A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) <-> A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) )
34 33 3anbi3i 
 |-  ( ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) <-> ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) )
35 34 abbii 
 |-  { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } = { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) }
36 35 unieqi 
 |-  U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } = U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) }
37 36 eleq2i 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } <-> U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } )
38 27 37 sylnib 
 |-  ( A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -. z e. z -> -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } )
39 26 38 ax-mp 
 |-  -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) }
40 dfon2lem2 
 |-  U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ A
41 1 40 ssexi 
 |-  U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. _V
42 41 snss 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } <-> { U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } )
43 39 42 mtbi 
 |-  -. { U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) }
44 43 intnan 
 |-  -. ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } /\ { U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } )
45 df-suc 
 |-  suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } = ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } u. { U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } } )
46 45 sseq1i 
 |-  ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } u. { U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } } ) C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } )
47 unss 
 |-  ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } /\ { U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } ) <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } u. { U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } } ) C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } )
48 46 47 bitr4i 
 |-  ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } /\ { U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } ) )
49 44 48 mtbir 
 |-  -. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) }
50 41 snss 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. A <-> { U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } } C_ A )
51 45 sseq1i 
 |-  ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ A <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } u. { U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } } ) C_ A )
52 unss 
 |-  ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ A /\ { U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } } C_ A ) <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } u. { U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } } ) C_ A )
53 51 52 bitr4i 
 |-  ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ A <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ A /\ { U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } } C_ A ) )
54 dfon2lem1 
 |-  Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) }
55 suctr 
 |-  ( Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } )
56 54 55 ax-mp 
 |-  Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) }
57 vex 
 |-  u e. _V
58 57 elsuc 
 |-  ( u e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } <-> ( u e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } \/ u = U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } ) )
59 eluni2 
 |-  ( u e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } <-> E. x e. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } u e. x )
60 nfa1 
 |-  F/ x A. x ( ( x C. u /\ Tr x ) -> x e. u )
61 32 rspccv 
 |-  ( A. t e. x A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( u e. x -> A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) )
62 psseq1 
 |-  ( y = x -> ( y C. u <-> x C. u ) )
63 treq 
 |-  ( y = x -> ( Tr y <-> Tr x ) )
64 62 63 anbi12d 
 |-  ( y = x -> ( ( y C. u /\ Tr y ) <-> ( x C. u /\ Tr x ) ) )
65 elequ1 
 |-  ( y = x -> ( y e. u <-> x e. u ) )
66 64 65 imbi12d 
 |-  ( y = x -> ( ( ( y C. u /\ Tr y ) -> y e. u ) <-> ( ( x C. u /\ Tr x ) -> x e. u ) ) )
67 66 cbvalvw 
 |-  ( A. y ( ( y C. u /\ Tr y ) -> y e. u ) <-> A. x ( ( x C. u /\ Tr x ) -> x e. u ) )
68 61 67 imbitrdi 
 |-  ( A. t e. x A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( u e. x -> A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) )
69 68 3ad2ant3 
 |-  ( ( x C_ A /\ Tr x /\ A. t e. x A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) -> ( u e. x -> A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) )
70 16 69 sylbi 
 |-  ( x e. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( u e. x -> A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) )
71 60 70 rexlimi 
 |-  ( E. x e. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } u e. x -> A. x ( ( x C. u /\ Tr x ) -> x e. u ) )
72 59 71 sylbi 
 |-  ( u e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> A. x ( ( x C. u /\ Tr x ) -> x e. u ) )
73 psseq1 
 |-  ( y = z -> ( y C. u <-> z C. u ) )
74 treq 
 |-  ( y = z -> ( Tr y <-> Tr z ) )
75 73 74 anbi12d 
 |-  ( y = z -> ( ( y C. u /\ Tr y ) <-> ( z C. u /\ Tr z ) ) )
76 elequ1 
 |-  ( y = z -> ( y e. u <-> z e. u ) )
77 75 76 imbi12d 
 |-  ( y = z -> ( ( ( y C. u /\ Tr y ) -> y e. u ) <-> ( ( z C. u /\ Tr z ) -> z e. u ) ) )
78 77 cbvalvw 
 |-  ( A. y ( ( y C. u /\ Tr y ) -> y e. u ) <-> A. z ( ( z C. u /\ Tr z ) -> z e. u ) )
79 61 78 imbitrdi 
 |-  ( A. t e. x A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( u e. x -> A. z ( ( z C. u /\ Tr z ) -> z e. u ) ) )
80 79 3ad2ant3 
 |-  ( ( x C_ A /\ Tr x /\ A. t e. x A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) -> ( u e. x -> A. z ( ( z C. u /\ Tr z ) -> z e. u ) ) )
81 16 80 sylbi 
 |-  ( x e. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( u e. x -> A. z ( ( z C. u /\ Tr z ) -> z e. u ) ) )
82 81 rexlimiv 
 |-  ( E. x e. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } u e. x -> A. z ( ( z C. u /\ Tr z ) -> z e. u ) )
83 59 82 sylbi 
 |-  ( u e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> A. z ( ( z C. u /\ Tr z ) -> z e. u ) )
84 83 rgen 
 |-  A. u e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } A. z ( ( z C. u /\ Tr z ) -> z e. u )
85 dfon2lem6 
 |-  ( ( Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } /\ A. u e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } A. z ( ( z C. u /\ Tr z ) -> z e. u ) ) -> A. x ( ( x C. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } /\ Tr x ) -> x e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } ) )
86 54 84 85 mp2an 
 |-  A. x ( ( x C. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } /\ Tr x ) -> x e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } )
87 psseq2 
 |-  ( u = U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( x C. u <-> x C. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } ) )
88 87 anbi1d 
 |-  ( u = U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( ( x C. u /\ Tr x ) <-> ( x C. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } /\ Tr x ) ) )
89 eleq2 
 |-  ( u = U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( x e. u <-> x e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } ) )
90 88 89 imbi12d 
 |-  ( u = U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( ( ( x C. u /\ Tr x ) -> x e. u ) <-> ( ( x C. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } /\ Tr x ) -> x e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } ) ) )
91 90 albidv 
 |-  ( u = U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( A. x ( ( x C. u /\ Tr x ) -> x e. u ) <-> A. x ( ( x C. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } /\ Tr x ) -> x e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } ) ) )
92 86 91 mpbiri 
 |-  ( u = U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> A. x ( ( x C. u /\ Tr x ) -> x e. u ) )
93 72 92 jaoi 
 |-  ( ( u e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } \/ u = U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } ) -> A. x ( ( x C. u /\ Tr x ) -> x e. u ) )
94 58 93 sylbi 
 |-  ( u e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> A. x ( ( x C. u /\ Tr x ) -> x e. u ) )
95 94 rgen 
 |-  A. u e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } A. x ( ( x C. u /\ Tr x ) -> x e. u )
96 41 sucex 
 |-  suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. _V
97 sseq1 
 |-  ( s = suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( s C_ A <-> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ A ) )
98 treq 
 |-  ( s = suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( Tr s <-> Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } ) )
99 raleq 
 |-  ( s = suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( A. u e. s A. x ( ( x C. u /\ Tr x ) -> x e. u ) <-> A. u e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) )
100 97 98 99 3anbi123d 
 |-  ( s = suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( ( s C_ A /\ Tr s /\ A. u e. s A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) <-> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ A /\ Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } /\ A. u e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) ) )
101 96 100 elab 
 |-  ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. { s | ( s C_ A /\ Tr s /\ A. u e. s A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) } <-> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ A /\ Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } /\ A. u e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) )
102 elssuni 
 |-  ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. { s | ( s C_ A /\ Tr s /\ A. u e. s A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) } -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ U. { s | ( s C_ A /\ Tr s /\ A. u e. s A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) } )
103 101 102 sylbir 
 |-  ( ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ A /\ Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } /\ A. u e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ U. { s | ( s C_ A /\ Tr s /\ A. u e. s A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) } )
104 56 95 103 mp3an23 
 |-  ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ A -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ U. { s | ( s C_ A /\ Tr s /\ A. u e. s A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) } )
105 sseq1 
 |-  ( s = w -> ( s C_ A <-> w C_ A ) )
106 treq 
 |-  ( s = w -> ( Tr s <-> Tr w ) )
107 raleq 
 |-  ( s = w -> ( A. u e. s A. x ( ( x C. u /\ Tr x ) -> x e. u ) <-> A. u e. w A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) )
108 psseq1 
 |-  ( x = y -> ( x C. u <-> y C. u ) )
109 treq 
 |-  ( x = y -> ( Tr x <-> Tr y ) )
110 108 109 anbi12d 
 |-  ( x = y -> ( ( x C. u /\ Tr x ) <-> ( y C. u /\ Tr y ) ) )
111 elequ1 
 |-  ( x = y -> ( x e. u <-> y e. u ) )
112 110 111 imbi12d 
 |-  ( x = y -> ( ( ( x C. u /\ Tr x ) -> x e. u ) <-> ( ( y C. u /\ Tr y ) -> y e. u ) ) )
113 112 cbvalvw 
 |-  ( A. x ( ( x C. u /\ Tr x ) -> x e. u ) <-> A. y ( ( y C. u /\ Tr y ) -> y e. u ) )
114 113 ralbii 
 |-  ( A. u e. w A. x ( ( x C. u /\ Tr x ) -> x e. u ) <-> A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) )
115 107 114 bitrdi 
 |-  ( s = w -> ( A. u e. s A. x ( ( x C. u /\ Tr x ) -> x e. u ) <-> A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) )
116 105 106 115 3anbi123d 
 |-  ( s = w -> ( ( s C_ A /\ Tr s /\ A. u e. s A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) <-> ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) ) )
117 116 cbvabv 
 |-  { s | ( s C_ A /\ Tr s /\ A. u e. s A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) } = { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) }
118 117 unieqi 
 |-  U. { s | ( s C_ A /\ Tr s /\ A. u e. s A. x ( ( x C. u /\ Tr x ) -> x e. u ) ) } = U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) }
119 104 118 sseqtrdi 
 |-  ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ A -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } )
120 119 a1i 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ A -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } ) )
121 53 120 biimtrrid 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ A /\ { U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } } C_ A ) -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } ) )
122 40 121 mpani 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( { U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } } C_ A -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } ) )
123 50 122 biimtrid 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. A -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ U. { w | ( w C_ A /\ Tr w /\ A. u e. w A. y ( ( y C. u /\ Tr y ) -> y e. u ) ) } ) )
124 49 123 mtoi 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. A )
125 psseq1 
 |-  ( x = U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( x C. A <-> U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C. A ) )
126 treq 
 |-  ( x = U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( Tr x <-> Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } ) )
127 125 126 anbi12d 
 |-  ( x = U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( ( x C. A /\ Tr x ) <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C. A /\ Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } ) ) )
128 eleq1 
 |-  ( x = U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( x e. A <-> U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. A ) )
129 127 128 imbi12d 
 |-  ( x = U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( ( ( x C. A /\ Tr x ) -> x e. A ) <-> ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C. A /\ Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. A ) ) )
130 41 129 spcv 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C. A /\ Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. A ) )
131 54 130 mpan2i 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C. A -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } e. A ) )
132 124 131 mtod 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C. A )
133 dfpss2 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C. A <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ A /\ -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } = A ) )
134 133 biimpri 
 |-  ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C_ A /\ -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } = A ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C. A )
135 40 134 mpan 
 |-  ( -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } = A -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } C. A )
136 132 135 nsyl2 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } = A )
137 eluni2 
 |-  ( z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } <-> E. x e. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } z e. x )
138 psseq2 
 |-  ( t = z -> ( y C. t <-> y C. z ) )
139 138 anbi1d 
 |-  ( t = z -> ( ( y C. t /\ Tr y ) <-> ( y C. z /\ Tr y ) ) )
140 elequ2 
 |-  ( t = z -> ( y e. t <-> y e. z ) )
141 139 140 imbi12d 
 |-  ( t = z -> ( ( ( y C. t /\ Tr y ) -> y e. t ) <-> ( ( y C. z /\ Tr y ) -> y e. z ) ) )
142 141 albidv 
 |-  ( t = z -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) <-> A. y ( ( y C. z /\ Tr y ) -> y e. z ) ) )
143 142 cbvralvw 
 |-  ( A. t e. x A. y ( ( y C. t /\ Tr y ) -> y e. t ) <-> A. z e. x A. y ( ( y C. z /\ Tr y ) -> y e. z ) )
144 14 143 bitrdi 
 |-  ( w = x -> ( A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) <-> A. z e. x A. y ( ( y C. z /\ Tr y ) -> y e. z ) ) )
145 12 13 144 3anbi123d 
 |-  ( w = x -> ( ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) <-> ( x C_ A /\ Tr x /\ A. z e. x A. y ( ( y C. z /\ Tr y ) -> y e. z ) ) ) )
146 11 145 elab 
 |-  ( x e. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } <-> ( x C_ A /\ Tr x /\ A. z e. x A. y ( ( y C. z /\ Tr y ) -> y e. z ) ) )
147 rsp 
 |-  ( A. z e. x A. y ( ( y C. z /\ Tr y ) -> y e. z ) -> ( z e. x -> A. y ( ( y C. z /\ Tr y ) -> y e. z ) ) )
148 147 3ad2ant3 
 |-  ( ( x C_ A /\ Tr x /\ A. z e. x A. y ( ( y C. z /\ Tr y ) -> y e. z ) ) -> ( z e. x -> A. y ( ( y C. z /\ Tr y ) -> y e. z ) ) )
149 146 148 sylbi 
 |-  ( x e. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> ( z e. x -> A. y ( ( y C. z /\ Tr y ) -> y e. z ) ) )
150 149 rexlimiv 
 |-  ( E. x e. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } z e. x -> A. y ( ( y C. z /\ Tr y ) -> y e. z ) )
151 137 150 sylbi 
 |-  ( z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } -> A. y ( ( y C. z /\ Tr y ) -> y e. z ) )
152 151 rgen 
 |-  A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } A. y ( ( y C. z /\ Tr y ) -> y e. z )
153 raleq 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } = A -> ( A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } A. y ( ( y C. z /\ Tr y ) -> y e. z ) <-> A. z e. A A. y ( ( y C. z /\ Tr y ) -> y e. z ) ) )
154 152 153 mpbii 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) } = A -> A. z e. A A. y ( ( y C. z /\ Tr y ) -> y e. z ) )
155 psseq2 
 |-  ( z = B -> ( y C. z <-> y C. B ) )
156 155 anbi1d 
 |-  ( z = B -> ( ( y C. z /\ Tr y ) <-> ( y C. B /\ Tr y ) ) )
157 eleq2 
 |-  ( z = B -> ( y e. z <-> y e. B ) )
158 156 157 imbi12d 
 |-  ( z = B -> ( ( ( y C. z /\ Tr y ) -> y e. z ) <-> ( ( y C. B /\ Tr y ) -> y e. B ) ) )
159 158 albidv 
 |-  ( z = B -> ( A. y ( ( y C. z /\ Tr y ) -> y e. z ) <-> A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) )
160 159 rspccv 
 |-  ( A. z e. A A. y ( ( y C. z /\ Tr y ) -> y e. z ) -> ( B e. A -> A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) )
161 136 154 160 3syl 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( B e. A -> A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) )