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 syl5ibr ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 → ∅ ≺ 𝐴 ) )
25 r10 ( 𝑅1 ‘ ∅ ) = ∅
26 25 breq1i ( ( 𝑅1 ‘ ∅ ) ≺ 𝐴 ↔ ∅ ≺ 𝐴 )
27 24 26 syl6ibr ( 𝐴 ∈ 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 syl5ibr ( ( 𝑥 ∈ On ∧ 𝑦𝑥 ) → ( 𝑧 ∈ ( card ‘ ( 𝑅1𝑦 ) ) → 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) )
164 163 reximdva ( 𝑥 ∈ On → ( ∃ 𝑦𝑥 𝑧 ∈ ( card ‘ ( 𝑅1𝑦 ) ) → ∃ 𝑦𝑥 𝑧 ⊆ ( ( ( card ∘ 𝑅1 ) ↾ 𝑥 ) ‘ 𝑦 ) ) )
165 159 164 syl5bi ( 𝑥 ∈ 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 syl5bi ( ( 𝑥 ∈ 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𝐴 ) ≈ 𝐴 )