Metamath Proof Explorer

Theorem tz9.12lem3

Description: Lemma for tz9.12 . (Contributed by NM, 22-Sep-2003) (Revised by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses tz9.12lem.1 
|- A e. _V
tz9.12lem.2 
|- F = ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } )
Assertion tz9.12lem3 
|- ( A. x e. A E. y e. On x e. ( R1 ` y ) -> A e. ( R1 ` suc suc U. ( F " A ) ) )

Proof

Step Hyp Ref Expression
1 tz9.12lem.1 
 |-  A e. _V
2 tz9.12lem.2 
 |-  F = ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } )
3 2 funmpt2 
 |-  Fun F
4 fveq2 
 |-  ( v = y -> ( R1 ` v ) = ( R1 ` y ) )
5 4 eleq2d 
 |-  ( v = y -> ( x e. ( R1 ` v ) <-> x e. ( R1 ` y ) ) )
6 5 rspcev 
 |-  ( ( y e. On /\ x e. ( R1 ` y ) ) -> E. v e. On x e. ( R1 ` v ) )
7 rabn0 
 |-  ( { v e. On | x e. ( R1 ` v ) } =/= (/) <-> E. v e. On x e. ( R1 ` v ) )
8 6 7 sylibr 
 |-  ( ( y e. On /\ x e. ( R1 ` y ) ) -> { v e. On | x e. ( R1 ` v ) } =/= (/) )
9 intex 
 |-  ( { v e. On | x e. ( R1 ` v ) } =/= (/) <-> |^| { v e. On | x e. ( R1 ` v ) } e. _V )
10 8 9 sylib 
 |-  ( ( y e. On /\ x e. ( R1 ` y ) ) -> |^| { v e. On | x e. ( R1 ` v ) } e. _V )
11 vex 
 |-  x e. _V
12 eleq1w 
 |-  ( z = x -> ( z e. ( R1 ` v ) <-> x e. ( R1 ` v ) ) )
13 12 rabbidv 
 |-  ( z = x -> { v e. On | z e. ( R1 ` v ) } = { v e. On | x e. ( R1 ` v ) } )
14 13 inteqd 
 |-  ( z = x -> |^| { v e. On | z e. ( R1 ` v ) } = |^| { v e. On | x e. ( R1 ` v ) } )
15 14 eleq1d 
 |-  ( z = x -> ( |^| { v e. On | z e. ( R1 ` v ) } e. _V <-> |^| { v e. On | x e. ( R1 ` v ) } e. _V ) )
16 2 dmmpt 
 |-  dom F = { z e. _V | |^| { v e. On | z e. ( R1 ` v ) } e. _V }
17 15 16 elrab2 
 |-  ( x e. dom F <-> ( x e. _V /\ |^| { v e. On | x e. ( R1 ` v ) } e. _V ) )
18 11 17 mpbiran 
 |-  ( x e. dom F <-> |^| { v e. On | x e. ( R1 ` v ) } e. _V )
19 10 18 sylibr 
 |-  ( ( y e. On /\ x e. ( R1 ` y ) ) -> x e. dom F )
20 funfvima 
 |-  ( ( Fun F /\ x e. dom F ) -> ( x e. A -> ( F ` x ) e. ( F " A ) ) )
21 3 19 20 sylancr 
 |-  ( ( y e. On /\ x e. ( R1 ` y ) ) -> ( x e. A -> ( F ` x ) e. ( F " A ) ) )
22 1 2 tz9.12lem2 
 |-  suc U. ( F " A ) e. On
23 1 2 tz9.12lem1 
 |-  ( F " A ) C_ On
24 onsucuni 
 |-  ( ( F " A ) C_ On -> ( F " A ) C_ suc U. ( F " A ) )
25 23 24 ax-mp 
 |-  ( F " A ) C_ suc U. ( F " A )
26 25 sseli 
 |-  ( ( F ` x ) e. ( F " A ) -> ( F ` x ) e. suc U. ( F " A ) )
27 r1ord2 
 |-  ( suc U. ( F " A ) e. On -> ( ( F ` x ) e. suc U. ( F " A ) -> ( R1 ` ( F ` x ) ) C_ ( R1 ` suc U. ( F " A ) ) ) )
28 22 26 27 mpsyl 
 |-  ( ( F ` x ) e. ( F " A ) -> ( R1 ` ( F ` x ) ) C_ ( R1 ` suc U. ( F " A ) ) )
29 21 28 syl6 
 |-  ( ( y e. On /\ x e. ( R1 ` y ) ) -> ( x e. A -> ( R1 ` ( F ` x ) ) C_ ( R1 ` suc U. ( F " A ) ) ) )
30 29 imp 
 |-  ( ( ( y e. On /\ x e. ( R1 ` y ) ) /\ x e. A ) -> ( R1 ` ( F ` x ) ) C_ ( R1 ` suc U. ( F " A ) ) )
31 14 2 fvmptg 
 |-  ( ( x e. _V /\ |^| { v e. On | x e. ( R1 ` v ) } e. _V ) -> ( F ` x ) = |^| { v e. On | x e. ( R1 ` v ) } )
32 11 31 mpan 
 |-  ( |^| { v e. On | x e. ( R1 ` v ) } e. _V -> ( F ` x ) = |^| { v e. On | x e. ( R1 ` v ) } )
33 9 32 sylbi 
 |-  ( { v e. On | x e. ( R1 ` v ) } =/= (/) -> ( F ` x ) = |^| { v e. On | x e. ( R1 ` v ) } )
34 ssrab2 
 |-  { v e. On | x e. ( R1 ` v ) } C_ On
35 onint 
 |-  ( ( { v e. On | x e. ( R1 ` v ) } C_ On /\ { v e. On | x e. ( R1 ` v ) } =/= (/) ) -> |^| { v e. On | x e. ( R1 ` v ) } e. { v e. On | x e. ( R1 ` v ) } )
36 34 35 mpan 
 |-  ( { v e. On | x e. ( R1 ` v ) } =/= (/) -> |^| { v e. On | x e. ( R1 ` v ) } e. { v e. On | x e. ( R1 ` v ) } )
37 33 36 eqeltrd 
 |-  ( { v e. On | x e. ( R1 ` v ) } =/= (/) -> ( F ` x ) e. { v e. On | x e. ( R1 ` v ) } )
38 fveq2 
 |-  ( y = ( F ` x ) -> ( R1 ` y ) = ( R1 ` ( F ` x ) ) )
39 38 eleq2d 
 |-  ( y = ( F ` x ) -> ( x e. ( R1 ` y ) <-> x e. ( R1 ` ( F ` x ) ) ) )
40 5 cbvrabv 
 |-  { v e. On | x e. ( R1 ` v ) } = { y e. On | x e. ( R1 ` y ) }
41 39 40 elrab2 
 |-  ( ( F ` x ) e. { v e. On | x e. ( R1 ` v ) } <-> ( ( F ` x ) e. On /\ x e. ( R1 ` ( F ` x ) ) ) )
42 41 simprbi 
 |-  ( ( F ` x ) e. { v e. On | x e. ( R1 ` v ) } -> x e. ( R1 ` ( F ` x ) ) )
43 8 37 42 3syl 
 |-  ( ( y e. On /\ x e. ( R1 ` y ) ) -> x e. ( R1 ` ( F ` x ) ) )
44 43 adantr 
 |-  ( ( ( y e. On /\ x e. ( R1 ` y ) ) /\ x e. A ) -> x e. ( R1 ` ( F ` x ) ) )
45 30 44 sseldd 
 |-  ( ( ( y e. On /\ x e. ( R1 ` y ) ) /\ x e. A ) -> x e. ( R1 ` suc U. ( F " A ) ) )
46 45 exp31 
 |-  ( y e. On -> ( x e. ( R1 ` y ) -> ( x e. A -> x e. ( R1 ` suc U. ( F " A ) ) ) ) )
47 46 com3r 
 |-  ( x e. A -> ( y e. On -> ( x e. ( R1 ` y ) -> x e. ( R1 ` suc U. ( F " A ) ) ) ) )
48 47 rexlimdv 
 |-  ( x e. A -> ( E. y e. On x e. ( R1 ` y ) -> x e. ( R1 ` suc U. ( F " A ) ) ) )
49 48 ralimia 
 |-  ( A. x e. A E. y e. On x e. ( R1 ` y ) -> A. x e. A x e. ( R1 ` suc U. ( F " A ) ) )
50 r1suc 
 |-  ( suc U. ( F " A ) e. On -> ( R1 ` suc suc U. ( F " A ) ) = ~P ( R1 ` suc U. ( F " A ) ) )
51 22 50 ax-mp 
 |-  ( R1 ` suc suc U. ( F " A ) ) = ~P ( R1 ` suc U. ( F " A ) )
52 51 eleq2i 
 |-  ( A e. ( R1 ` suc suc U. ( F " A ) ) <-> A e. ~P ( R1 ` suc U. ( F " A ) ) )
53 1 elpw 
 |-  ( A e. ~P ( R1 ` suc U. ( F " A ) ) <-> A C_ ( R1 ` suc U. ( F " A ) ) )
54 dfss3 
 |-  ( A C_ ( R1 ` suc U. ( F " A ) ) <-> A. x e. A x e. ( R1 ` suc U. ( F " A ) ) )
55 52 53 54 3bitri 
 |-  ( A e. ( R1 ` suc suc U. ( F " A ) ) <-> A. x e. A x e. ( R1 ` suc U. ( F " A ) ) )
56 49 55 sylibr 
 |-  ( A. x e. A E. y e. On x e. ( R1 ` y ) -> A e. ( R1 ` suc suc U. ( F " A ) ) )