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