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