Metamath Proof Explorer

Theorem r1ordg

Description: Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of TakeutiZaring p. 77. (Contributed by NM, 8-Sep-2003)

Ref Expression
Assertion r1ordg 
|- ( B e. dom R1 -> ( A e. B -> ( R1 ` A ) e. ( R1 ` B ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( B e. dom R1 /\ A e. B ) -> B e. dom R1 )
2 r1dmlim 
 |-  Lim dom R1
3 limord 
 |-  ( Lim dom R1 -> Ord dom R1 )
4 2 3 ax-mp 
 |-  Ord dom R1
5 ordsson 
 |-  ( Ord dom R1 -> dom R1 C_ On )
6 4 5 ax-mp 
 |-  dom R1 C_ On
7 6 sseli 
 |-  ( B e. dom R1 -> B e. On )
8 1 7 syl 
 |-  ( ( B e. dom R1 /\ A e. B ) -> B e. On )
9 onelon 
 |-  ( ( B e. On /\ A e. B ) -> A e. On )
10 7 9 sylan 
 |-  ( ( B e. dom R1 /\ A e. B ) -> A e. On )
11 onsuc 
 |-  ( A e. On -> suc A e. On )
12 10 11 syl 
 |-  ( ( B e. dom R1 /\ A e. B ) -> suc A e. On )
13 eloni 
 |-  ( B e. On -> Ord B )
14 ordsucss 
 |-  ( Ord B -> ( A e. B -> suc A C_ B ) )
15 13 14 syl 
 |-  ( B e. On -> ( A e. B -> suc A C_ B ) )
16 15 imp 
 |-  ( ( B e. On /\ A e. B ) -> suc A C_ B )
17 7 16 sylan 
 |-  ( ( B e. dom R1 /\ A e. B ) -> suc A C_ B )
18 eleq1 
 |-  ( x = suc A -> ( x e. dom R1 <-> suc A e. dom R1 ) )
19 fveq2 
 |-  ( x = suc A -> ( R1 ` x ) = ( R1 ` suc A ) )
20 19 eleq2d 
 |-  ( x = suc A -> ( ( R1 ` A ) e. ( R1 ` x ) <-> ( R1 ` A ) e. ( R1 ` suc A ) ) )
21 18 20 imbi12d 
 |-  ( x = suc A -> ( ( x e. dom R1 -> ( R1 ` A ) e. ( R1 ` x ) ) <-> ( suc A e. dom R1 -> ( R1 ` A ) e. ( R1 ` suc A ) ) ) )
22 eleq1 
 |-  ( x = y -> ( x e. dom R1 <-> y e. dom R1 ) )
23 fveq2 
 |-  ( x = y -> ( R1 ` x ) = ( R1 ` y ) )
24 23 eleq2d 
 |-  ( x = y -> ( ( R1 ` A ) e. ( R1 ` x ) <-> ( R1 ` A ) e. ( R1 ` y ) ) )
25 22 24 imbi12d 
 |-  ( x = y -> ( ( x e. dom R1 -> ( R1 ` A ) e. ( R1 ` x ) ) <-> ( y e. dom R1 -> ( R1 ` A ) e. ( R1 ` y ) ) ) )
26 eleq1 
 |-  ( x = suc y -> ( x e. dom R1 <-> suc y e. dom R1 ) )
27 fveq2 
 |-  ( x = suc y -> ( R1 ` x ) = ( R1 ` suc y ) )
28 27 eleq2d 
 |-  ( x = suc y -> ( ( R1 ` A ) e. ( R1 ` x ) <-> ( R1 ` A ) e. ( R1 ` suc y ) ) )
29 26 28 imbi12d 
 |-  ( x = suc y -> ( ( x e. dom R1 -> ( R1 ` A ) e. ( R1 ` x ) ) <-> ( suc y e. dom R1 -> ( R1 ` A ) e. ( R1 ` suc y ) ) ) )
30 eleq1 
 |-  ( x = B -> ( x e. dom R1 <-> B e. dom R1 ) )
31 fveq2 
 |-  ( x = B -> ( R1 ` x ) = ( R1 ` B ) )
32 31 eleq2d 
 |-  ( x = B -> ( ( R1 ` A ) e. ( R1 ` x ) <-> ( R1 ` A ) e. ( R1 ` B ) ) )
33 30 32 imbi12d 
 |-  ( x = B -> ( ( x e. dom R1 -> ( R1 ` A ) e. ( R1 ` x ) ) <-> ( B e. dom R1 -> ( R1 ` A ) e. ( R1 ` B ) ) ) )
34 fvex 
 |-  ( R1 ` A ) e. _V
35 34 pwid 
 |-  ( R1 ` A ) e. ~P ( R1 ` A )
36 limsuc 
 |-  ( Lim dom R1 -> ( A e. dom R1 <-> suc A e. dom R1 ) )
37 2 36 ax-mp 
 |-  ( A e. dom R1 <-> suc A e. dom R1 )
38 r1sucg 
 |-  ( A e. dom R1 -> ( R1 ` suc A ) = ~P ( R1 ` A ) )
39 37 38 sylbir 
 |-  ( suc A e. dom R1 -> ( R1 ` suc A ) = ~P ( R1 ` A ) )
40 35 39 eleqtrrid 
 |-  ( suc A e. dom R1 -> ( R1 ` A ) e. ( R1 ` suc A ) )
41 40 a1i 
 |-  ( suc A e. On -> ( suc A e. dom R1 -> ( R1 ` A ) e. ( R1 ` suc A ) ) )
42 limsuc 
 |-  ( Lim dom R1 -> ( y e. dom R1 <-> suc y e. dom R1 ) )
43 2 42 ax-mp 
 |-  ( y e. dom R1 <-> suc y e. dom R1 )
44 r1tr 
 |-  Tr ( R1 ` y )
45 dftr4 
 |-  ( Tr ( R1 ` y ) <-> ( R1 ` y ) C_ ~P ( R1 ` y ) )
46 44 45 mpbi 
 |-  ( R1 ` y ) C_ ~P ( R1 ` y )
47 r1sucg 
 |-  ( y e. dom R1 -> ( R1 ` suc y ) = ~P ( R1 ` y ) )
48 46 47 sseqtrrid 
 |-  ( y e. dom R1 -> ( R1 ` y ) C_ ( R1 ` suc y ) )
49 48 sseld 
 |-  ( y e. dom R1 -> ( ( R1 ` A ) e. ( R1 ` y ) -> ( R1 ` A ) e. ( R1 ` suc y ) ) )
50 49 a2i 
 |-  ( ( y e. dom R1 -> ( R1 ` A ) e. ( R1 ` y ) ) -> ( y e. dom R1 -> ( R1 ` A ) e. ( R1 ` suc y ) ) )
51 43 50 biimtrrid 
 |-  ( ( y e. dom R1 -> ( R1 ` A ) e. ( R1 ` y ) ) -> ( suc y e. dom R1 -> ( R1 ` A ) e. ( R1 ` suc y ) ) )
52 51 a1i 
 |-  ( ( ( y e. On /\ suc A e. On ) /\ suc A C_ y ) -> ( ( y e. dom R1 -> ( R1 ` A ) e. ( R1 ` y ) ) -> ( suc y e. dom R1 -> ( R1 ` A ) e. ( R1 ` suc y ) ) ) )
53 simprl 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> suc A C_ x )
54 simplr 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> suc A e. On )
55 onsucb 
 |-  ( A e. On <-> suc A e. On )
56 54 55 sylibr 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> A e. On )
57 limord 
 |-  ( Lim x -> Ord x )
58 57 ad2antrr 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> Ord x )
59 ordelsuc 
 |-  ( ( A e. On /\ Ord x ) -> ( A e. x <-> suc A C_ x ) )
60 56 58 59 syl2anc 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> ( A e. x <-> suc A C_ x ) )
61 53 60 mpbird 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> A e. x )
62 limsuc 
 |-  ( Lim x -> ( A e. x <-> suc A e. x ) )
63 62 ad2antrr 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> ( A e. x <-> suc A e. x ) )
64 61 63 mpbid 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> suc A e. x )
65 simprr 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> x e. dom R1 )
66 ordtr1 
 |-  ( Ord dom R1 -> ( ( A e. x /\ x e. dom R1 ) -> A e. dom R1 ) )
67 4 66 ax-mp 
 |-  ( ( A e. x /\ x e. dom R1 ) -> A e. dom R1 )
68 61 65 67 syl2anc 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> A e. dom R1 )
69 68 38 syl 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> ( R1 ` suc A ) = ~P ( R1 ` A ) )
70 35 69 eleqtrrid 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> ( R1 ` A ) e. ( R1 ` suc A ) )
71 fveq2 
 |-  ( y = suc A -> ( R1 ` y ) = ( R1 ` suc A ) )
72 71 eleq2d 
 |-  ( y = suc A -> ( ( R1 ` A ) e. ( R1 ` y ) <-> ( R1 ` A ) e. ( R1 ` suc A ) ) )
73 72 rspcev 
 |-  ( ( suc A e. x /\ ( R1 ` A ) e. ( R1 ` suc A ) ) -> E. y e. x ( R1 ` A ) e. ( R1 ` y ) )
74 64 70 73 syl2anc 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> E. y e. x ( R1 ` A ) e. ( R1 ` y ) )
75 eliun 
 |-  ( ( R1 ` A ) e. U_ y e. x ( R1 ` y ) <-> E. y e. x ( R1 ` A ) e. ( R1 ` y ) )
76 74 75 sylibr 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> ( R1 ` A ) e. U_ y e. x ( R1 ` y ) )
77 simpll 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> Lim x )
78 r1limg 
 |-  ( ( x e. dom R1 /\ Lim x ) -> ( R1 ` x ) = U_ y e. x ( R1 ` y ) )
79 65 77 78 syl2anc 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> ( R1 ` x ) = U_ y e. x ( R1 ` y ) )
80 76 79 eleqtrrd 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ ( suc A C_ x /\ x e. dom R1 ) ) -> ( R1 ` A ) e. ( R1 ` x ) )
81 80 expr 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) -> ( x e. dom R1 -> ( R1 ` A ) e. ( R1 ` x ) ) )
82 81 a1d 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) -> ( A. y e. x ( suc A C_ y -> ( y e. dom R1 -> ( R1 ` A ) e. ( R1 ` y ) ) ) -> ( x e. dom R1 -> ( R1 ` A ) e. ( R1 ` x ) ) ) )
83 21 25 29 33 41 52 82 tfindsg 
 |-  ( ( ( B e. On /\ suc A e. On ) /\ suc A C_ B ) -> ( B e. dom R1 -> ( R1 ` A ) e. ( R1 ` B ) ) )
84 83 impr 
 |-  ( ( ( B e. On /\ suc A e. On ) /\ ( suc A C_ B /\ B e. dom R1 ) ) -> ( R1 ` A ) e. ( R1 ` B ) )
85 8 12 17 1 84 syl22anc 
 |-  ( ( B e. dom R1 /\ A e. B ) -> ( R1 ` A ) e. ( R1 ` B ) )
86 85 ex 
 |-  ( B e. dom R1 -> ( A e. B -> ( R1 ` A ) e. ( R1 ` B ) ) )