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