Metamath Proof Explorer

Theorem inar1

Description: ( R1A ) for A a strongly inaccessible cardinal is equipotent to A . (Contributed by Mario Carneiro, 6-Jun-2013)

Ref Expression
Assertion inar1 ( 𝐴 ∈ Inacc → ( 𝑅1 ‘ 𝐴 ) ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 inawina ⊢ ( 𝐴 ∈ Inacc → 𝐴 ∈ Inaccw )
2 winaon ⊢ ( 𝐴 ∈ Inaccw → 𝐴 ∈ On )
3 1 2 syl ⊢ ( 𝐴 ∈ Inacc → 𝐴 ∈ On )
4 winalim ⊢ ( 𝐴 ∈ Inaccw → Lim 𝐴 )
5 1 4 syl ⊢ ( 𝐴 ∈ Inacc → Lim 𝐴 )
6 r1lim ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) )
7 3 5 6 syl2anc ⊢ ( 𝐴 ∈ Inacc → ( 𝑅1 ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) )
8 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
9 3 8 sylan ⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
10 eleq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ 𝐴 ↔ ∅ ∈ 𝐴 ) )
11 fveq2 ⊢ ( 𝑥 = ∅ → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ ∅ ) )
12 11 breq1d ⊢ ( 𝑥 = ∅ → ( ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ↔ ( 𝑅1 ‘ ∅ ) ≺ 𝐴 ) )
13 10 12 imbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) ↔ ( ∅ ∈ 𝐴 → ( 𝑅1 ‘ ∅ ) ≺ 𝐴 ) ) )
14 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
15 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) )
16 15 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ↔ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) )
17 14 16 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) ↔ ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) )
18 eleq1 ⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴 ) )
19 fveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ suc 𝑦 ) )
20 19 breq1d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ↔ ( 𝑅1 ‘ suc 𝑦 ) ≺ 𝐴 ) )
21 18 20 imbi12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) ↔ ( suc 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ suc 𝑦 ) ≺ 𝐴 ) ) )
22 ne0i ⊢ ( ∅ ∈ 𝐴 → 𝐴 ≠ ∅ )
23 0sdomg ⊢ ( 𝐴 ∈ On → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
24 22 23 imbitrrid ⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 → ∅ ≺ 𝐴 ) )
25 r10 ⊢ ( 𝑅1 ‘ ∅ ) = ∅
26 25 breq1i ⊢ ( ( 𝑅1 ‘ ∅ ) ≺ 𝐴 ↔ ∅ ≺ 𝐴 )
27 24 26 imbitrrdi ⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 → ( 𝑅1 ‘ ∅ ) ≺ 𝐴 ) )
28 1 2 27 3syl ⊢ ( 𝐴 ∈ Inacc → ( ∅ ∈ 𝐴 → ( 𝑅1 ‘ ∅ ) ≺ 𝐴 ) )
29 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
30 ordtr ⊢ ( Ord 𝐴 → Tr 𝐴 )
31 29 30 syl ⊢ ( 𝐴 ∈ On → Tr 𝐴 )
32 trsuc ⊢ ( ( Tr 𝐴 ∧ suc 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
33 32 ex ⊢ ( Tr 𝐴 → ( suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) )
34 3 31 33 3syl ⊢ ( 𝐴 ∈ Inacc → ( suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) )
35 34 adantl ⊢ ( ( 𝑦 ∈ On ∧ 𝐴 ∈ Inacc ) → ( suc 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) )
36 r1suc ⊢ ( 𝑦 ∈ On → ( 𝑅1 ‘ suc 𝑦 ) = 𝒫 ( 𝑅1 ‘ 𝑦 ) )
37 fvex ⊢ ( 𝑅1 ‘ 𝑦 ) ∈ V
38 37 cardid ⊢ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≈ ( 𝑅1 ‘ 𝑦 )
39 38 ensymi ⊢ ( 𝑅1 ‘ 𝑦 ) ≈ ( card ‘ ( 𝑅1 ‘ 𝑦 ) )
40 pwen ⊢ ( ( 𝑅1 ‘ 𝑦 ) ≈ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → 𝒫 ( 𝑅1 ‘ 𝑦 ) ≈ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
41 39 40 ax-mp ⊢ 𝒫 ( 𝑅1 ‘ 𝑦 ) ≈ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) )
42 36 41 eqbrtrdi ⊢ ( 𝑦 ∈ On → ( 𝑅1 ‘ suc 𝑦 ) ≈ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
43 winacard ⊢ ( 𝐴 ∈ Inaccw → ( card ‘ 𝐴 ) = 𝐴 )
44 43 eleq2d ⊢ ( 𝐴 ∈ Inaccw → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ 𝐴 ) ↔ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ) )
45 cardsdom ⊢ ( ( ( 𝑅1 ‘ 𝑦 ) ∈ V ∧ 𝐴 ∈ On ) → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ 𝐴 ) ↔ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) )
46 37 2 45 sylancr ⊢ ( 𝐴 ∈ Inaccw → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ 𝐴 ) ↔ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) )
47 44 46 bitr3d ⊢ ( 𝐴 ∈ Inaccw → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ↔ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) )
48 1 47 syl ⊢ ( 𝐴 ∈ Inacc → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ↔ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) )
49 elina ⊢ ( 𝐴 ∈ Inacc ↔ ( 𝐴 ≠ ∅ ∧ ( cf ‘ 𝐴 ) = 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴 ) )
50 49 simp3bi ⊢ ( 𝐴 ∈ Inacc → ∀ 𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴 )
51 pweq ⊢ ( 𝑧 = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → 𝒫 𝑧 = 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
52 51 breq1d ⊢ ( 𝑧 = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝒫 𝑧 ≺ 𝐴 ↔ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≺ 𝐴 ) )
53 52 rspccv ⊢ ( ∀ 𝑧 ∈ 𝐴 𝒫 𝑧 ≺ 𝐴 → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 → 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≺ 𝐴 ) )
54 50 53 syl ⊢ ( 𝐴 ∈ Inacc → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 → 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≺ 𝐴 ) )
55 48 54 sylbird ⊢ ( 𝐴 ∈ Inacc → ( ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 → 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≺ 𝐴 ) )
56 55 imp ⊢ ( ( 𝐴 ∈ Inacc ∧ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≺ 𝐴 )
57 ensdomtr ⊢ ( ( ( 𝑅1 ‘ suc 𝑦 ) ≈ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∧ 𝒫 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≺ 𝐴 ) → ( 𝑅1 ‘ suc 𝑦 ) ≺ 𝐴 )
58 42 56 57 syl2an ⊢ ( ( 𝑦 ∈ On ∧ ( 𝐴 ∈ Inacc ∧ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) → ( 𝑅1 ‘ suc 𝑦 ) ≺ 𝐴 )
59 58 expr ⊢ ( ( 𝑦 ∈ On ∧ 𝐴 ∈ Inacc ) → ( ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 → ( 𝑅1 ‘ suc 𝑦 ) ≺ 𝐴 ) )
60 35 59 imim12d ⊢ ( ( 𝑦 ∈ On ∧ 𝐴 ∈ Inacc ) → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ( suc 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ suc 𝑦 ) ≺ 𝐴 ) ) )
61 60 ex ⊢ ( 𝑦 ∈ On → ( 𝐴 ∈ Inacc → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ( suc 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ suc 𝑦 ) ≺ 𝐴 ) ) ) )
62 vex ⊢ 𝑥 ∈ V
63 r1lim ⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → ( 𝑅1 ‘ 𝑥 ) = ∪ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) )
64 62 63 mpan ⊢ ( Lim 𝑥 → ( 𝑅1 ‘ 𝑥 ) = ∪ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) )
65 nfcv ⊢ Ⅎ 𝑦 𝑧
66 nfcv ⊢ Ⅎ 𝑦 ( 𝑅1 ‘ 𝑧 )
67 nfcv ⊢ Ⅎ 𝑦 ≼
68 nfiu1 ⊢ Ⅎ 𝑦 ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) )
69 66 67 68 nfbr ⊢ Ⅎ 𝑦 ( 𝑅1 ‘ 𝑧 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) )
70 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑅1 ‘ 𝑦 ) = ( 𝑅1 ‘ 𝑧 ) )
71 70 breq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑅1 ‘ 𝑦 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ↔ ( 𝑅1 ‘ 𝑧 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
72 fvex ⊢ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ V
73 62 72 iunex ⊢ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ V
74 ssiun2 ⊢ ( 𝑦 ∈ 𝑥 → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
75 ssdomg ⊢ ( ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ V → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
76 73 74 75 mpsyl ⊢ ( 𝑦 ∈ 𝑥 → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
77 endomtr ⊢ ( ( ( 𝑅1 ‘ 𝑦 ) ≈ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∧ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝑅1 ‘ 𝑦 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
78 39 76 77 sylancr ⊢ ( 𝑦 ∈ 𝑥 → ( 𝑅1 ‘ 𝑦 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
79 65 69 71 78 vtoclgaf ⊢ ( 𝑧 ∈ 𝑥 → ( 𝑅1 ‘ 𝑧 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
80 79 rgen ⊢ ∀ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) )
81 iundom ⊢ ( ( 𝑥 ∈ V ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ≼ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ∪ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ≼ ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
82 62 80 81 mp2an ⊢ ∪ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ≼ ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
83 62 73 unex ⊢ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ V
84 ssun2 ⊢ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
85 ssdomg ⊢ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ V → ( ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) )
86 83 84 85 mp2 ⊢ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
87 62 xpdom2 ⊢ ( ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( 𝑥 × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) )
88 86 87 ax-mp ⊢ ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( 𝑥 × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
89 ssun1 ⊢ 𝑥 ⊆ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
90 ssdomg ⊢ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ V → ( 𝑥 ⊆ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → 𝑥 ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) )
91 83 89 90 mp2 ⊢ 𝑥 ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
92 83 xpdom1 ⊢ ( 𝑥 ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝑥 × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ≼ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) )
93 91 92 ax-mp ⊢ ( 𝑥 × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ≼ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
94 domtr ⊢ ( ( ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( 𝑥 × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ∧ ( 𝑥 × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ≼ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ) → ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) )
95 88 93 94 mp2an ⊢ ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
96 limomss ⊢ ( Lim 𝑥 → ω ⊆ 𝑥 )
97 96 89 sstrdi ⊢ ( Lim 𝑥 → ω ⊆ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
98 ssdomg ⊢ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ V → ( ω ⊆ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ω ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) )
99 83 97 98 mpsyl ⊢ ( Lim 𝑥 → ω ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
100 infxpidm ⊢ ( ω ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ≈ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
101 99 100 syl ⊢ ( Lim 𝑥 → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ≈ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
102 domentr ⊢ ( ( ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ∧ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) × ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) ≈ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) → ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
103 95 101 102 sylancr ⊢ ( Lim 𝑥 → ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
104 domtr ⊢ ( ( ∪ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ≼ ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∧ ( 𝑥 × ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) → ∪ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
105 82 103 104 sylancr ⊢ ( Lim 𝑥 → ∪ 𝑧 ∈ 𝑥 ( 𝑅1 ‘ 𝑧 ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
106 64 105 eqbrtrd ⊢ ( Lim 𝑥 → ( 𝑅1 ‘ 𝑥 ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
107 106 ad2antlr ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝑅1 ‘ 𝑥 ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
108 eleq1a ⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 = 𝑥 → 𝐴 ∈ 𝐴 ) )
109 ordirr ⊢ ( Ord 𝐴 → ¬ 𝐴 ∈ 𝐴 )
110 3 29 109 3syl ⊢ ( 𝐴 ∈ Inacc → ¬ 𝐴 ∈ 𝐴 )
111 108 110 nsyli ⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 ∈ Inacc → ¬ 𝐴 = 𝑥 ) )
112 111 imp ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ Inacc ) → ¬ 𝐴 = 𝑥 )
113 112 ad2ant2r ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ¬ 𝐴 = 𝑥 )
114 simpll ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → 𝑥 ∈ 𝐴 )
115 limord ⊢ ( Lim 𝑥 → Ord 𝑥 )
116 62 elon ⊢ ( 𝑥 ∈ On ↔ Ord 𝑥 )
117 115 116 sylibr ⊢ ( Lim 𝑥 → 𝑥 ∈ On )
118 117 ad2antlr ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → 𝑥 ∈ On )
119 cardf ⊢ card : V ⟶ On
120 r1fnon ⊢ 𝑅1 Fn On
121 dffn2 ⊢ ( 𝑅1 Fn On ↔ 𝑅1 : On ⟶ V )
122 120 121 mpbi ⊢ 𝑅1 : On ⟶ V
123 fco ⊢ ( ( card : V ⟶ On ∧ 𝑅1 : On ⟶ V ) → ( card ∘ 𝑅1 ) : On ⟶ On )
124 119 122 123 mp2an ⊢ ( card ∘ 𝑅1 ) : On ⟶ On
125 onss ⊢ ( 𝑥 ∈ On → 𝑥 ⊆ On )
126 fssres ⊢ ( ( ( card ∘ 𝑅1 ) : On ⟶ On ∧ 𝑥 ⊆ On ) → ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ On )
127 124 125 126 sylancr ⊢ ( 𝑥 ∈ On → ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ On )
128 ffn ⊢ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ On → ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) Fn 𝑥 )
129 118 127 128 3syl ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) Fn 𝑥 )
130 3 ad2antlr ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → 𝐴 ∈ On )
131 simpr ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
132 simplll ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ 𝐴 )
133 ontr1 ⊢ ( 𝐴 ∈ On → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) )
134 133 imp ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) ) → 𝑦 ∈ 𝐴 )
135 130 131 132 134 syl12anc ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝐴 )
136 37 130 45 sylancr ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ 𝐴 ) ↔ ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) )
137 1 43 syl ⊢ ( 𝐴 ∈ Inacc → ( card ‘ 𝐴 ) = 𝐴 )
138 137 ad2antlr ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( card ‘ 𝐴 ) = 𝐴 )
139 138 eleq2d ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ ( card ‘ 𝐴 ) ↔ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ) )
140 136 139 bitr3d ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ↔ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ) )
141 140 biimpd ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ) )
142 135 141 embantd ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ) )
143 117 ad2antlr ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) → 𝑥 ∈ On )
144 fvres ⊢ ( 𝑦 ∈ 𝑥 → ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) = ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) )
145 144 adantl ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) = ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) )
146 onelon ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
147 fvco3 ⊢ ( ( 𝑅1 : On ⟶ V ∧ 𝑦 ∈ On ) → ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
148 122 146 147 sylancr ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ( card ∘ 𝑅1 ) ‘ 𝑦 ) = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
149 145 148 eqtrd ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
150 143 149 sylan ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) = ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
151 150 eleq1d ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ∈ 𝐴 ↔ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 ) )
152 142 151 sylibrd ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ∈ 𝐴 ) )
153 152 ralimdva ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ∀ 𝑦 ∈ 𝑥 ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ∈ 𝐴 ) )
154 153 impr ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ∀ 𝑦 ∈ 𝑥 ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ∈ 𝐴 )
155 ffnfv ⊢ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ 𝐴 ↔ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ∈ 𝐴 ) )
156 129 154 155 sylanbrc ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ 𝐴 )
157 eleq2 ⊢ ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
158 157 biimpa ⊢ ( ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
159 eliun ⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ↔ ∃ 𝑦 ∈ 𝑥 𝑧 ∈ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
160 cardon ⊢ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On
161 160 onelssi ⊢ ( 𝑧 ∈ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → 𝑧 ⊆ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
162 149 sseq2d ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ↔ 𝑧 ⊆ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
163 161 162 imbitrrid ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( 𝑧 ∈ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) )
164 163 reximdva ⊢ ( 𝑥 ∈ On → ( ∃ 𝑦 ∈ 𝑥 𝑧 ∈ ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) )
165 159 164 biimtrid ⊢ ( 𝑥 ∈ On → ( 𝑧 ∈ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) )
166 158 165 syl5 ⊢ ( 𝑥 ∈ On → ( ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) )
167 166 expdimp ⊢ ( ( 𝑥 ∈ On ∧ 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝑧 ∈ 𝐴 → ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) )
168 167 ralrimiv ⊢ ( ( 𝑥 ∈ On ∧ 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) )
169 168 ex ⊢ ( 𝑥 ∈ On → ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) )
170 118 169 syl ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) )
171 ffun ⊢ ( ( card ∘ 𝑅1 ) : On ⟶ On → Fun ( card ∘ 𝑅1 ) )
172 124 171 ax-mp ⊢ Fun ( card ∘ 𝑅1 )
173 resfunexg ⊢ ( ( Fun ( card ∘ 𝑅1 ) ∧ 𝑥 ∈ V ) → ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ∈ V )
174 172 62 173 mp2an ⊢ ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ∈ V
175 feq1 ⊢ ( 𝑤 = ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) → ( 𝑤 : 𝑥 ⟶ 𝐴 ↔ ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ 𝐴 ) )
176 fveq1 ⊢ ( 𝑤 = ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) → ( 𝑤 ‘ 𝑦 ) = ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) )
177 176 sseq2d ⊢ ( 𝑤 = ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) → ( 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ↔ 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) )
178 177 rexbidv ⊢ ( 𝑤 = ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) → ( ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) )
179 178 ralbidv ⊢ ( 𝑤 = ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) )
180 175 179 anbi12d ⊢ ( 𝑤 = ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) → ( ( 𝑤 : 𝑥 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ) ↔ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) ) )
181 174 180 spcev ⊢ ( ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) : 𝑥 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) → ∃ 𝑤 ( 𝑤 : 𝑥 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ) )
182 156 170 181 syl6an ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ∃ 𝑤 ( 𝑤 : 𝑥 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ) ) )
183 3 ad2antrl ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → 𝐴 ∈ On )
184 cfflb ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( ∃ 𝑤 ( 𝑤 : 𝑥 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ) → ( cf ‘ 𝐴 ) ⊆ 𝑥 ) )
185 183 118 184 syl2anc ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ∃ 𝑤 ( 𝑤 : 𝑥 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝑥 𝑧 ⊆ ( 𝑤 ‘ 𝑦 ) ) → ( cf ‘ 𝐴 ) ⊆ 𝑥 ) )
186 182 185 syld ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ( cf ‘ 𝐴 ) ⊆ 𝑥 ) )
187 49 simp2bi ⊢ ( 𝐴 ∈ Inacc → ( cf ‘ 𝐴 ) = 𝐴 )
188 187 sseq1d ⊢ ( 𝐴 ∈ Inacc → ( ( cf ‘ 𝐴 ) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥 ) )
189 188 ad2antrl ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( cf ‘ 𝐴 ) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥 ) )
190 186 189 sylibd ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → 𝐴 ⊆ 𝑥 ) )
191 ontri1 ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴 ) )
192 183 118 191 syl2anc ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ 𝐴 ) )
193 190 192 sylibd ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) → ¬ 𝑥 ∈ 𝐴 ) )
194 114 193 mt2d ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ¬ 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
195 iunon ⊢ ( ( 𝑥 ∈ V ∧ ∀ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On ) → ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On )
196 62 195 mpan ⊢ ( ∀ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On → ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On )
197 160 a1i ⊢ ( 𝑦 ∈ 𝑥 → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On )
198 196 197 mprg ⊢ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On
199 eqcom ⊢ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 ↔ 𝐴 = ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
200 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
201 eloni ⊢ ( ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On → Ord ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
202 ordequn ⊢ ( ( Ord 𝑥 ∧ Ord ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝐴 = ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) )
203 200 201 202 syl2an ⊢ ( ( 𝑥 ∈ On ∧ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On ) → ( 𝐴 = ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) )
204 199 203 biimtrid ⊢ ( ( 𝑥 ∈ On ∧ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 → ( 𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) )
205 118 198 204 sylancl ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 → ( 𝐴 = 𝑥 ∨ 𝐴 = ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ) )
206 113 194 205 mtord ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ¬ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 )
207 onelss ⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴 ) )
208 183 114 207 sylc ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → 𝑥 ⊆ 𝐴 )
209 onelss ⊢ ( 𝐴 ∈ On → ( ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ 𝐴 → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ 𝐴 ) )
210 130 142 209 sylsyld ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ 𝐴 ) )
211 210 ralimdva ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ 𝐴 ∈ Inacc ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ∀ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ 𝐴 ) )
212 211 impr ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ∀ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ 𝐴 )
213 iunss ⊢ ( ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ 𝐴 ↔ ∀ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ 𝐴 )
214 212 213 sylibr ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ⊆ 𝐴 )
215 208 214 unssd ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ⊆ 𝐴 )
216 id ⊢ ( 𝑥 = if ( 𝑥 ∈ On , 𝑥 , ∅ ) → 𝑥 = if ( 𝑥 ∈ On , 𝑥 , ∅ ) )
217 iuneq1 ⊢ ( 𝑥 = if ( 𝑥 ∈ On , 𝑥 , ∅ ) → ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) = ∪ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) )
218 216 217 uneq12d ⊢ ( 𝑥 = if ( 𝑥 ∈ On , 𝑥 , ∅ ) → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = ( if ( 𝑥 ∈ On , 𝑥 , ∅ ) ∪ ∪ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) )
219 218 eleq1d ⊢ ( 𝑥 = if ( 𝑥 ∈ On , 𝑥 , ∅ ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ On ↔ ( if ( 𝑥 ∈ On , 𝑥 , ∅ ) ∪ ∪ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ On ) )
220 0elon ⊢ ∅ ∈ On
221 220 elimel ⊢ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ∈ On
222 221 elexi ⊢ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ∈ V
223 iunon ⊢ ( ( if ( 𝑥 ∈ On , 𝑥 , ∅ ) ∈ V ∧ ∀ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On ) → ∪ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On )
224 222 223 mpan ⊢ ( ∀ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On → ∪ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On )
225 160 a1i ⊢ ( 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) → ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On )
226 224 225 mprg ⊢ ∪ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ∈ On
227 221 226 onun2i ⊢ ( if ( 𝑥 ∈ On , 𝑥 , ∅ ) ∪ ∪ 𝑦 ∈ if ( 𝑥 ∈ On , 𝑥 , ∅ ) ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ On
228 219 227 dedth ⊢ ( 𝑥 ∈ On → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ On )
229 117 228 syl ⊢ ( Lim 𝑥 → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ On )
230 229 adantl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ On )
231 3 adantr ⊢ ( ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) → 𝐴 ∈ On )
232 onsseleq ⊢ ( ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ⊆ 𝐴 ↔ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 ∨ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 ) ) )
233 230 231 232 syl2an ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ⊆ 𝐴 ↔ ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 ∨ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 ) ) )
234 215 233 mpbid ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 ∨ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 ) )
235 234 orcomd ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 ∨ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 ) )
236 235 ord ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ¬ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) = 𝐴 → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 ) )
237 206 236 mpd ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 )
238 137 ad2antrl ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( card ‘ 𝐴 ) = 𝐴 )
239 iscard ⊢ ( ( card ‘ 𝐴 ) = 𝐴 ↔ ( 𝐴 ∈ On ∧ ∀ 𝑧 ∈ 𝐴 𝑧 ≺ 𝐴 ) )
240 239 simprbi ⊢ ( ( card ‘ 𝐴 ) = 𝐴 → ∀ 𝑧 ∈ 𝐴 𝑧 ≺ 𝐴 )
241 breq1 ⊢ ( 𝑧 = ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) → ( 𝑧 ≺ 𝐴 ↔ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≺ 𝐴 ) )
242 241 rspccv ⊢ ( ∀ 𝑧 ∈ 𝐴 𝑧 ≺ 𝐴 → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≺ 𝐴 ) )
243 238 240 242 3syl ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∈ 𝐴 → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≺ 𝐴 ) )
244 237 243 mpd ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≺ 𝐴 )
245 domsdomtr ⊢ ( ( ( 𝑅1 ‘ 𝑥 ) ≼ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ∧ ( 𝑥 ∪ ∪ 𝑦 ∈ 𝑥 ( card ‘ ( 𝑅1 ‘ 𝑦 ) ) ) ≺ 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 )
246 107 244 245 syl2anc ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ Lim 𝑥 ) ∧ ( 𝐴 ∈ Inacc ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) ) ) → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 )
247 246 exp43 ⊢ ( 𝑥 ∈ 𝐴 → ( Lim 𝑥 → ( 𝐴 ∈ Inacc → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) ) ) )
248 247 com4l ⊢ ( Lim 𝑥 → ( 𝐴 ∈ Inacc → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝑅1 ‘ 𝑦 ) ≺ 𝐴 ) → ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) ) ) )
249 13 17 21 28 61 248 tfinds2 ⊢ ( 𝑥 ∈ On → ( 𝐴 ∈ Inacc → ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) ) )
250 249 impd ⊢ ( 𝑥 ∈ On → ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 ) )
251 9 250 mpcom ⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 )
252 sdomdom ⊢ ( ( 𝑅1 ‘ 𝑥 ) ≺ 𝐴 → ( 𝑅1 ‘ 𝑥 ) ≼ 𝐴 )
253 251 252 syl ⊢ ( ( 𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) ≼ 𝐴 )
254 253 ralrimiva ⊢ ( 𝐴 ∈ Inacc → ∀ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ≼ 𝐴 )
255 iundom ⊢ ( ( 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ≼ 𝐴 ) → ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ≼ ( 𝐴 × 𝐴 ) )
256 3 254 255 syl2anc ⊢ ( 𝐴 ∈ Inacc → ∪ 𝑥 ∈ 𝐴 ( 𝑅1 ‘ 𝑥 ) ≼ ( 𝐴 × 𝐴 ) )
257 7 256 eqbrtrd ⊢ ( 𝐴 ∈ Inacc → ( 𝑅1 ‘ 𝐴 ) ≼ ( 𝐴 × 𝐴 ) )
258 winainf ⊢ ( 𝐴 ∈ Inaccw → ω ⊆ 𝐴 )
259 1 258 syl ⊢ ( 𝐴 ∈ Inacc → ω ⊆ 𝐴 )
260 infxpen ⊢ ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )
261 3 259 260 syl2anc ⊢ ( 𝐴 ∈ Inacc → ( 𝐴 × 𝐴 ) ≈ 𝐴 )
262 domentr ⊢ ( ( ( 𝑅1 ‘ 𝐴 ) ≼ ( 𝐴 × 𝐴 ) ∧ ( 𝐴 × 𝐴 ) ≈ 𝐴 ) → ( 𝑅1 ‘ 𝐴 ) ≼ 𝐴 )
263 257 261 262 syl2anc ⊢ ( 𝐴 ∈ Inacc → ( 𝑅1 ‘ 𝐴 ) ≼ 𝐴 )
264 fvex ⊢ ( 𝑅1 ‘ 𝐴 ) ∈ V
265 122 fdmi ⊢ dom 𝑅1 = On
266 2 265 eleqtrrdi ⊢ ( 𝐴 ∈ Inaccw → 𝐴 ∈ dom 𝑅1 )
267 onssr1 ⊢ ( 𝐴 ∈ dom 𝑅1 → 𝐴 ⊆ ( 𝑅1 ‘ 𝐴 ) )
268 1 266 267 3syl ⊢ ( 𝐴 ∈ Inacc → 𝐴 ⊆ ( 𝑅1 ‘ 𝐴 ) )
269 ssdomg ⊢ ( ( 𝑅1 ‘ 𝐴 ) ∈ V → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝐴 ) → 𝐴 ≼ ( 𝑅1 ‘ 𝐴 ) ) )
270 264 268 269 mpsyl ⊢ ( 𝐴 ∈ Inacc → 𝐴 ≼ ( 𝑅1 ‘ 𝐴 ) )
271 sbth ⊢ ( ( ( 𝑅1 ‘ 𝐴 ) ≼ 𝐴 ∧ 𝐴 ≼ ( 𝑅1 ‘ 𝐴 ) ) → ( 𝑅1 ‘ 𝐴 ) ≈ 𝐴 )
272 263 270 271 syl2anc ⊢ ( 𝐴 ∈ Inacc → ( 𝑅1 ‘ 𝐴 ) ≈ 𝐴 )