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 ( 𝐵 ∈ dom 𝑅1 → ( 𝐴 ∈ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝐴 ∈ 𝐵 ) → 𝐵 ∈ dom 𝑅1 )
2 r1funlim ⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
3 2 simpri ⊢ Lim dom 𝑅1
4 limord ⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
5 3 4 ax-mp ⊢ Ord dom 𝑅1
6 ordsson ⊢ ( Ord dom 𝑅1 → dom 𝑅1 ⊆ On )
7 5 6 ax-mp ⊢ dom 𝑅1 ⊆ On
8 7 sseli ⊢ ( 𝐵 ∈ dom 𝑅1 → 𝐵 ∈ On )
9 1 8 syl ⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝐴 ∈ 𝐵 ) → 𝐵 ∈ On )
10 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ On )
11 8 10 sylan ⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ On )
12 suceloni ⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On )
13 11 12 syl ⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝐴 ∈ 𝐵 ) → suc 𝐴 ∈ On )
14 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
15 ordsucss ⊢ ( Ord 𝐵 → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )
16 14 15 syl ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵 ) )
17 16 imp ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ 𝐵 ) → suc 𝐴 ⊆ 𝐵 )
18 8 17 sylan ⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝐴 ∈ 𝐵 ) → suc 𝐴 ⊆ 𝐵 )
19 eleq1 ⊢ ( 𝑥 = suc 𝐴 → ( 𝑥 ∈ dom 𝑅1 ↔ suc 𝐴 ∈ dom 𝑅1 ) )
20 fveq2 ⊢ ( 𝑥 = suc 𝐴 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ suc 𝐴 ) )
21 20 eleq2d ⊢ ( 𝑥 = suc 𝐴 → ( ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝐴 ) ) )
22 19 21 imbi12d ⊢ ( 𝑥 = suc 𝐴 → ( ( 𝑥 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑥 ) ) ↔ ( suc 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝐴 ) ) ) )
23 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ dom 𝑅1 ↔ 𝑦 ∈ dom 𝑅1 ) )
24 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) )
25 24 eleq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑦 ) ) )
26 23 25 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑥 ) ) ↔ ( 𝑦 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑦 ) ) ) )
27 eleq1 ⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1 ) )
28 fveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ suc 𝑦 ) )
29 28 eleq2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝑦 ) ) )
30 27 29 imbi12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑥 ) ) ↔ ( suc 𝑦 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝑦 ) ) ) )
31 eleq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ dom 𝑅1 ↔ 𝐵 ∈ dom 𝑅1 ) )
32 fveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝐵 ) )
33 32 eleq2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) ) )
34 31 33 imbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑥 ) ) ↔ ( 𝐵 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) ) ) )
35 fvex ⊢ ( 𝑅1 ‘ 𝐴 ) ∈ V
36 35 pwid ⊢ ( 𝑅1 ‘ 𝐴 ) ∈ 𝒫 ( 𝑅1 ‘ 𝐴 )
37 limsuc ⊢ ( Lim dom 𝑅1 → ( 𝐴 ∈ dom 𝑅1 ↔ suc 𝐴 ∈ dom 𝑅1 ) )
38 3 37 ax-mp ⊢ ( 𝐴 ∈ dom 𝑅1 ↔ suc 𝐴 ∈ dom 𝑅1 )
39 r1sucg ⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝐴 ) = 𝒫 ( 𝑅1 ‘ 𝐴 ) )
40 38 39 sylbir ⊢ ( suc 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝐴 ) = 𝒫 ( 𝑅1 ‘ 𝐴 ) )
41 36 40 eleqtrrid ⊢ ( suc 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝐴 ) )
42 41 a1i ⊢ ( suc 𝐴 ∈ On → ( suc 𝐴 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝐴 ) ) )
43 limsuc ⊢ ( Lim dom 𝑅1 → ( 𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1 ) )
44 3 43 ax-mp ⊢ ( 𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1 )
45 r1tr ⊢ Tr ( 𝑅1 ‘ 𝑦 )
46 dftr4 ⊢ ( Tr ( 𝑅1 ‘ 𝑦 ) ↔ ( 𝑅1 ‘ 𝑦 ) ⊆ 𝒫 ( 𝑅1 ‘ 𝑦 ) )
47 45 46 mpbi ⊢ ( 𝑅1 ‘ 𝑦 ) ⊆ 𝒫 ( 𝑅1 ‘ 𝑦 )
48 r1sucg ⊢ ( 𝑦 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝑦 ) = 𝒫 ( 𝑅1 ‘ 𝑦 ) )
49 47 48 sseqtrrid ⊢ ( 𝑦 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝑦 ) ⊆ ( 𝑅1 ‘ suc 𝑦 ) )
50 49 sseld ⊢ ( 𝑦 ∈ dom 𝑅1 → ( ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑦 ) → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝑦 ) ) )
51 50 a2i ⊢ ( ( 𝑦 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝑦 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝑦 ) ) )
52 44 51 syl5bir ⊢ ( ( 𝑦 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑦 ) ) → ( suc 𝑦 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝑦 ) ) )
53 52 a1i ⊢ ( ( ( 𝑦 ∈ On ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑦 ) → ( ( 𝑦 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑦 ) ) → ( suc 𝑦 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝑦 ) ) ) )
54 simprl ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → suc 𝐴 ⊆ 𝑥 )
55 simplr ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → suc 𝐴 ∈ On )
56 sucelon ⊢ ( 𝐴 ∈ On ↔ suc 𝐴 ∈ On )
57 55 56 sylibr ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → 𝐴 ∈ On )
58 limord ⊢ ( Lim 𝑥 → Ord 𝑥 )
59 58 ad2antrr ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → Ord 𝑥 )
60 ordelsuc ⊢ ( ( 𝐴 ∈ On ∧ Ord 𝑥 ) → ( 𝐴 ∈ 𝑥 ↔ suc 𝐴 ⊆ 𝑥 ) )
61 57 59 60 syl2anc ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → ( 𝐴 ∈ 𝑥 ↔ suc 𝐴 ⊆ 𝑥 ) )
62 54 61 mpbird ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → 𝐴 ∈ 𝑥 )
63 limsuc ⊢ ( Lim 𝑥 → ( 𝐴 ∈ 𝑥 ↔ suc 𝐴 ∈ 𝑥 ) )
64 63 ad2antrr ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → ( 𝐴 ∈ 𝑥 ↔ suc 𝐴 ∈ 𝑥 ) )
65 62 64 mpbid ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → suc 𝐴 ∈ 𝑥 )
66 simprr ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → 𝑥 ∈ dom 𝑅1 )
67 ordtr1 ⊢ ( Ord dom 𝑅1 → ( ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) → 𝐴 ∈ dom 𝑅1 ) )
68 5 67 ax-mp ⊢ ( ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) → 𝐴 ∈ dom 𝑅1 )
69 62 66 68 syl2anc ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → 𝐴 ∈ dom 𝑅1 )
70 69 39 syl ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → ( 𝑅1 ‘ suc 𝐴 ) = 𝒫 ( 𝑅1 ‘ 𝐴 ) )
71 36 70 eleqtrrid ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝐴 ) )
72 fveq2 ⊢ ( 𝑦 = suc 𝐴 → ( 𝑅1 ‘ 𝑦 ) = ( 𝑅1 ‘ suc 𝐴 ) )
73 72 eleq2d ⊢ ( 𝑦 = suc 𝐴 → ( ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑦 ) ↔ ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝐴 ) ) )
74 73 rspcev ⊢ ( ( suc 𝐴 ∈ 𝑥 ∧ ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ suc 𝐴 ) ) → ∃ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑦 ) )
75 65 71 74 syl2anc ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → ∃ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑦 ) )
76 eliun ⊢ ( ( 𝑅1 ‘ 𝐴 ) ∈ ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑦 ) )
77 75 76 sylibr ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → ( 𝑅1 ‘ 𝐴 ) ∈ ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) )
78 simpll ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → Lim 𝑥 )
79 r1limg ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ Lim 𝑥 ) → ( 𝑅1 ‘ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) )
80 66 78 79 syl2anc ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → ( 𝑅1 ‘ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝑅1 ‘ 𝑦 ) )
81 77 80 eleqtrrd ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) ) → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑥 ) )
82 81 expr ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) → ( 𝑥 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑥 ) ) )
83 82 a1d ⊢ ( ( ( Lim 𝑥 ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( suc 𝐴 ⊆ 𝑦 → ( 𝑦 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝑥 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑥 ) ) ) )
84 22 26 30 34 42 53 83 tfindsg ⊢ ( ( ( 𝐵 ∈ On ∧ suc 𝐴 ∈ On ) ∧ suc 𝐴 ⊆ 𝐵 ) → ( 𝐵 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) ) )
85 84 impr ⊢ ( ( ( 𝐵 ∈ On ∧ suc 𝐴 ∈ On ) ∧ ( suc 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ dom 𝑅1 ) ) → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) )
86 9 13 18 1 85 syl22anc ⊢ ( ( 𝐵 ∈ dom 𝑅1 ∧ 𝐴 ∈ 𝐵 ) → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) )
87 86 ex ⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝐴 ∈ 𝐵 → ( 𝑅1 ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝐵 ) ) )