Metamath Proof Explorer

Theorem rankonidlem

Description: Lemma for rankonid . (Contributed by NM, 14-Oct-2003) (Revised by Mario Carneiro, 22-Mar-2013)

Ref Expression
Assertion rankonidlem ( 𝐴 ∈ dom 𝑅1 → ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 r1dmlim ⊢ Lim dom 𝑅1
2 limord ⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
3 1 2 ax-mp ⊢ Ord dom 𝑅1
4 ordelon ⊢ ( ( Ord dom 𝑅1 ∧ 𝐴 ∈ dom 𝑅1 ) → 𝐴 ∈ On )
5 3 4 mpan ⊢ ( 𝐴 ∈ dom 𝑅1 → 𝐴 ∈ On )
6 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ dom 𝑅1 ↔ 𝑦 ∈ dom 𝑅1 ) )
7 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) )
8 fveq2 ⊢ ( 𝑥 = 𝑦 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) )
9 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
10 8 9 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( rank ‘ 𝑥 ) = 𝑥 ↔ ( rank ‘ 𝑦 ) = 𝑦 ) )
11 7 10 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑥 ) = 𝑥 ) ↔ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) )
12 6 11 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ dom 𝑅1 → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑥 ) = 𝑥 ) ) ↔ ( 𝑦 ∈ dom 𝑅1 → ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) ) )
13 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ dom 𝑅1 ↔ 𝐴 ∈ dom 𝑅1 ) )
14 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) )
15 fveq2 ⊢ ( 𝑥 = 𝐴 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝐴 ) )
16 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
17 15 16 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( rank ‘ 𝑥 ) = 𝑥 ↔ ( rank ‘ 𝐴 ) = 𝐴 ) )
18 14 17 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑥 ) = 𝑥 ) ↔ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = 𝐴 ) ) )
19 13 18 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ dom 𝑅1 → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑥 ) = 𝑥 ) ) ↔ ( 𝐴 ∈ dom 𝑅1 → ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = 𝐴 ) ) ) )
20 ordtr1 ⊢ ( Ord dom 𝑅1 → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) → 𝑦 ∈ dom 𝑅1 ) )
21 3 20 ax-mp ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ dom 𝑅1 ) → 𝑦 ∈ dom 𝑅1 )
22 21 ancoms ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ dom 𝑅1 )
23 pm5.5 ⊢ ( 𝑦 ∈ dom 𝑅1 → ( ( 𝑦 ∈ dom 𝑅1 → ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) ↔ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) )
24 22 23 syl ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ∈ dom 𝑅1 → ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) ↔ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) )
25 24 ralbidva ⊢ ( 𝑥 ∈ dom 𝑅1 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ dom 𝑅1 → ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) )
26 simplr ⊢ ( ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → 𝑦 ∈ 𝑥 )
27 ordelon ⊢ ( ( Ord dom 𝑅1 ∧ 𝑥 ∈ dom 𝑅1 ) → 𝑥 ∈ On )
28 3 27 mpan ⊢ ( 𝑥 ∈ dom 𝑅1 → 𝑥 ∈ On )
29 28 ad2antrr ⊢ ( ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → 𝑥 ∈ On )
30 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
31 29 30 syl ⊢ ( ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → Ord 𝑥 )
32 ordelsuc ⊢ ( ( 𝑦 ∈ 𝑥 ∧ Ord 𝑥 ) → ( 𝑦 ∈ 𝑥 ↔ suc 𝑦 ⊆ 𝑥 ) )
33 26 31 32 syl2anc ⊢ ( ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → ( 𝑦 ∈ 𝑥 ↔ suc 𝑦 ⊆ 𝑥 ) )
34 26 33 mpbid ⊢ ( ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → suc 𝑦 ⊆ 𝑥 )
35 22 adantr ⊢ ( ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → 𝑦 ∈ dom 𝑅1 )
36 limsuc ⊢ ( Lim dom 𝑅1 → ( 𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1 ) )
37 1 36 ax-mp ⊢ ( 𝑦 ∈ dom 𝑅1 ↔ suc 𝑦 ∈ dom 𝑅1 )
38 35 37 sylib ⊢ ( ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → suc 𝑦 ∈ dom 𝑅1 )
39 simpll ⊢ ( ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → 𝑥 ∈ dom 𝑅1 )
40 r1ord3g ⊢ ( ( suc 𝑦 ∈ dom 𝑅1 ∧ 𝑥 ∈ dom 𝑅1 ) → ( suc 𝑦 ⊆ 𝑥 → ( 𝑅1 ‘ suc 𝑦 ) ⊆ ( 𝑅1 ‘ 𝑥 ) ) )
41 38 39 40 syl2anc ⊢ ( ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → ( suc 𝑦 ⊆ 𝑥 → ( 𝑅1 ‘ suc 𝑦 ) ⊆ ( 𝑅1 ‘ 𝑥 ) ) )
42 34 41 mpd ⊢ ( ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → ( 𝑅1 ‘ suc 𝑦 ) ⊆ ( 𝑅1 ‘ 𝑥 ) )
43 rankidb ⊢ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) → 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
44 43 ad2antrl ⊢ ( ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) )
45 suceq ⊢ ( ( rank ‘ 𝑦 ) = 𝑦 → suc ( rank ‘ 𝑦 ) = suc 𝑦 )
46 45 ad2antll ⊢ ( ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → suc ( rank ‘ 𝑦 ) = suc 𝑦 )
47 46 fveq2d ⊢ ( ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) = ( 𝑅1 ‘ suc 𝑦 ) )
48 44 47 eleqtrd ⊢ ( ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → 𝑦 ∈ ( 𝑅1 ‘ suc 𝑦 ) )
49 42 48 sseldd ⊢ ( ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) )
50 49 ex ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) → 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
51 50 ralimdva ⊢ ( 𝑥 ∈ dom 𝑅1 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
52 51 imp ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) )
53 dfss3 ⊢ ( 𝑥 ⊆ ( 𝑅1 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) )
54 52 53 sylibr ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → 𝑥 ⊆ ( 𝑅1 ‘ 𝑥 ) )
55 vex ⊢ 𝑥 ∈ V
56 55 elpw ⊢ ( 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) ↔ 𝑥 ⊆ ( 𝑅1 ‘ 𝑥 ) )
57 54 56 sylibr ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → 𝑥 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) )
58 r1sucg ⊢ ( 𝑥 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
59 58 adantr ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
60 57 59 eleqtrrd ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → 𝑥 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
61 r1elwf ⊢ ( 𝑥 ∈ ( 𝑅1 ‘ suc 𝑥 ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
62 60 61 syl ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
63 rankval3b ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝑥 ) = ∩ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ 𝑥 ( rank ‘ 𝑦 ) ∈ 𝑧 } )
64 62 63 syl ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → ( rank ‘ 𝑥 ) = ∩ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ 𝑥 ( rank ‘ 𝑦 ) ∈ 𝑧 } )
65 eleq1 ⊢ ( ( rank ‘ 𝑦 ) = 𝑦 → ( ( rank ‘ 𝑦 ) ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) )
66 65 adantl ⊢ ( ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) → ( ( rank ‘ 𝑦 ) ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) )
67 66 ralimi ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) → ∀ 𝑦 ∈ 𝑥 ( ( rank ‘ 𝑦 ) ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) )
68 ralbi ⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( rank ‘ 𝑦 ) ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → ( ∀ 𝑦 ∈ 𝑥 ( rank ‘ 𝑦 ) ∈ 𝑧 ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝑧 ) )
69 67 68 syl ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) → ( ∀ 𝑦 ∈ 𝑥 ( rank ‘ 𝑦 ) ∈ 𝑧 ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝑧 ) )
70 dfss3 ⊢ ( 𝑥 ⊆ 𝑧 ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝑧 )
71 69 70 bitr4di ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) → ( ∀ 𝑦 ∈ 𝑥 ( rank ‘ 𝑦 ) ∈ 𝑧 ↔ 𝑥 ⊆ 𝑧 ) )
72 71 rabbidv ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) → { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ 𝑥 ( rank ‘ 𝑦 ) ∈ 𝑧 } = { 𝑧 ∈ On ∣ 𝑥 ⊆ 𝑧 } )
73 72 inteqd ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) → ∩ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ 𝑥 ( rank ‘ 𝑦 ) ∈ 𝑧 } = ∩ { 𝑧 ∈ On ∣ 𝑥 ⊆ 𝑧 } )
74 73 adantl ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → ∩ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ 𝑥 ( rank ‘ 𝑦 ) ∈ 𝑧 } = ∩ { 𝑧 ∈ On ∣ 𝑥 ⊆ 𝑧 } )
75 28 adantr ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → 𝑥 ∈ On )
76 intmin ⊢ ( 𝑥 ∈ On → ∩ { 𝑧 ∈ On ∣ 𝑥 ⊆ 𝑧 } = 𝑥 )
77 75 76 syl ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → ∩ { 𝑧 ∈ On ∣ 𝑥 ⊆ 𝑧 } = 𝑥 )
78 64 74 77 3eqtrd ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → ( rank ‘ 𝑥 ) = 𝑥 )
79 62 78 jca ⊢ ( ( 𝑥 ∈ dom 𝑅1 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑥 ) = 𝑥 ) )
80 79 ex ⊢ ( 𝑥 ∈ dom 𝑅1 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑥 ) = 𝑥 ) ) )
81 25 80 sylbid ⊢ ( 𝑥 ∈ dom 𝑅1 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ dom 𝑅1 → ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑥 ) = 𝑥 ) ) )
82 81 com12 ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ dom 𝑅1 → ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → ( 𝑥 ∈ dom 𝑅1 → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑥 ) = 𝑥 ) ) )
83 82 a1i ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ dom 𝑅1 → ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑦 ) = 𝑦 ) ) → ( 𝑥 ∈ dom 𝑅1 → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑥 ) = 𝑥 ) ) ) )
84 12 19 83 tfis3 ⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ dom 𝑅1 → ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = 𝐴 ) ) )
85 5 84 mpcom ⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = 𝐴 ) )