# 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 ${⊢}{A}\in \mathrm{Inacc}\to {R}_{1}\left({A}\right)\approx {A}$

### Proof

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