Theorem infxpenlem

Description: Lemma for infxpen . (Contributed by Mario Carneiro, 9-Mar-2013) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	leweon.1	$$⊢L=\left\{⟨x,y⟩|\left(\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(x\right)\in 1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\in 2^{nd}\left(y\right)\right)\right)\right)\right\}$$
	r0weon.1	$$⊢R=\left\{⟨z,w⟩|\left(\left(z\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge w\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \left(1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)\vee \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\wedge zLw\right)\right)\right)\right\}$$
	infxpen.1	$$⊢Q=R\cap \left(\left(a\times a\right)\times \left(a\times a\right)\right)$$
	infxpen.2	$$⊢\phi \leftrightarrow \left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \forall m\in am\prec a\right)\right)$$
	infxpen.3	$$⊢M=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)$$
	infxpen.4	$$⊢J=OrdIso\left(Q,a\times a\right)$$
Assertion	infxpenlem	$$⊢\left(A\in \mathrm{On}\wedge \mathrm{\omega }\subseteq A\right)\to \left(A\times A\right)\approx A$$

Proof

Step	Hyp	Ref	Expression
1		leweon.1	$$⊢L=\left\{⟨x,y⟩|\left(\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(x\right)\in 1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\in 2^{nd}\left(y\right)\right)\right)\right)\right\}$$
2		r0weon.1	$$⊢R=\left\{⟨z,w⟩|\left(\left(z\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge w\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \left(1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)\vee \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\wedge zLw\right)\right)\right)\right\}$$
3		infxpen.1	$$⊢Q=R\cap \left(\left(a\times a\right)\times \left(a\times a\right)\right)$$
4		infxpen.2	$$⊢\phi \leftrightarrow \left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \forall m\in am\prec a\right)\right)$$
5		infxpen.3	$$⊢M=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)$$
6		infxpen.4	$$⊢J=OrdIso\left(Q,a\times a\right)$$
7		sseq2	$$⊢a=m\to \left(\mathrm{\omega }\subseteq a\leftrightarrow \mathrm{\omega }\subseteq m\right)$$
8		xpeq12	$$⊢\left(a=m\wedge a=m\right)\to a\times a=m\times m$$
9	8	anidms	$$⊢a=m\to a\times a=m\times m$$
10		id	$$⊢a=m\to a=m$$
11	9 10	breq12d	$$⊢a=m\to \left(\left(a\times a\right)\approx a\leftrightarrow \left(m\times m\right)\approx m\right)$$
12	7 11	imbi12d	$$⊢a=m\to \left(\left(\mathrm{\omega }\subseteq a\to \left(a\times a\right)\approx a\right)\leftrightarrow \left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)$$
13		sseq2	$$⊢a=A\to \left(\mathrm{\omega }\subseteq a\leftrightarrow \mathrm{\omega }\subseteq A\right)$$
14		xpeq12	$$⊢\left(a=A\wedge a=A\right)\to a\times a=A\times A$$
15	14	anidms	$$⊢a=A\to a\times a=A\times A$$
16		id	$$⊢a=A\to a=A$$
17	15 16	breq12d	$$⊢a=A\to \left(\left(a\times a\right)\approx a\leftrightarrow \left(A\times A\right)\approx A\right)$$
18	13 17	imbi12d	$$⊢a=A\to \left(\left(\mathrm{\omega }\subseteq a\to \left(a\times a\right)\approx a\right)\leftrightarrow \left(\mathrm{\omega }\subseteq A\to \left(A\times A\right)\approx A\right)\right)$$
19		vex	$$⊢a\in \mathrm{V}$$
20	19 19	xpex	$$⊢a\times a\in \mathrm{V}$$
21		simpll	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \forall m\in am\prec a\right)\right)\to a\in \mathrm{On}$$
22	4 21	sylbi	$$⊢\phi \to a\in \mathrm{On}$$
23		onss	$$⊢a\in \mathrm{On}\to a\subseteq \mathrm{On}$$
24	22 23	syl	$$⊢\phi \to a\subseteq \mathrm{On}$$
25		xpss12	$$⊢\left(a\subseteq \mathrm{On}\wedge a\subseteq \mathrm{On}\right)\to a\times a\subseteq \mathrm{On}\times \mathrm{On}$$
26	24 24 25	syl2anc	$$⊢\phi \to a\times a\subseteq \mathrm{On}\times \mathrm{On}$$
27	1 2	r0weon	$$⊢\left(R\mathrm{We}\left(\mathrm{On}\times \mathrm{On}\right)\wedge R\mathrm{Se}\left(\mathrm{On}\times \mathrm{On}\right)\right)$$
28	27	simpli	$$⊢R\mathrm{We}\left(\mathrm{On}\times \mathrm{On}\right)$$
29		wess	$$⊢a\times a\subseteq \mathrm{On}\times \mathrm{On}\to \left(R\mathrm{We}\left(\mathrm{On}\times \mathrm{On}\right)\to R\mathrm{We}\left(a\times a\right)\right)$$
30	26 28 29	mpisyl	$$⊢\phi \to R\mathrm{We}\left(a\times a\right)$$
31		weinxp	$$⊢R\mathrm{We}\left(a\times a\right)\leftrightarrow \left(R\cap \left(\left(a\times a\right)\times \left(a\times a\right)\right)\right)\mathrm{We}\left(a\times a\right)$$
32	30 31	sylib	$$⊢\phi \to \left(R\cap \left(\left(a\times a\right)\times \left(a\times a\right)\right)\right)\mathrm{We}\left(a\times a\right)$$
33		weeq1	$$⊢Q=R\cap \left(\left(a\times a\right)\times \left(a\times a\right)\right)\to \left(Q\mathrm{We}\left(a\times a\right)\leftrightarrow \left(R\cap \left(\left(a\times a\right)\times \left(a\times a\right)\right)\right)\mathrm{We}\left(a\times a\right)\right)$$
34	3 33	ax-mp	$$⊢Q\mathrm{We}\left(a\times a\right)\leftrightarrow \left(R\cap \left(\left(a\times a\right)\times \left(a\times a\right)\right)\right)\mathrm{We}\left(a\times a\right)$$
35	32 34	sylibr	$$⊢\phi \to Q\mathrm{We}\left(a\times a\right)$$
36	6	oiiso	$$⊢\left(a\times a\in \mathrm{V}\wedge Q\mathrm{We}\left(a\times a\right)\right)\to J{Isom}_{\mathrm{E},Q}\left(\mathrm{dom}J,a\times a\right)$$
37	20 35 36	sylancr	$$⊢\phi \to J{Isom}_{\mathrm{E},Q}\left(\mathrm{dom}J,a\times a\right)$$
38		isof1o	$$⊢J{Isom}_{\mathrm{E},Q}\left(\mathrm{dom}J,a\times a\right)\to J:\mathrm{dom}J\underset{1-1\; onto}{⟶}a\times a$$
39		f1ocnv	$$⊢J:\mathrm{dom}J\underset{1-1\; onto}{⟶}a\times a\to J^{-1}:a\times a\underset{1-1\; onto}{⟶}\mathrm{dom}J$$
40		f1of1	$$⊢J^{-1}:a\times a\underset{1-1\; onto}{⟶}\mathrm{dom}J\to J^{-1}:a\times a\underset{1-1}{⟶}\mathrm{dom}J$$
41	37 38 39 40	4syl	$$⊢\phi \to J^{-1}:a\times a\underset{1-1}{⟶}\mathrm{dom}J$$
42		f1f1orn	$$⊢J^{-1}:a\times a\underset{1-1}{⟶}\mathrm{dom}J\to J^{-1}:a\times a\underset{1-1\; onto}{⟶}\mathrm{ran}{J}^{-1}$$
43	20	f1oen	$$⊢J^{-1}:a\times a\underset{1-1\; onto}{⟶}\mathrm{ran}{J}^{-1}\to \left(a\times a\right)\approx \mathrm{ran}{J}^{-1}$$
44	41 42 43	3syl	$$⊢\phi \to \left(a\times a\right)\approx \mathrm{ran}{J}^{-1}$$
45		f1ofn	$$⊢J^{-1}:a\times a\underset{1-1\; onto}{⟶}\mathrm{dom}J\to J^{-1}Fn\left(a\times a\right)$$
46	37 38 39 45	4syl	$$⊢\phi \to J^{-1}Fn\left(a\times a\right)$$
47	37	adantr	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to J{Isom}_{\mathrm{E},Q}\left(\mathrm{dom}J,a\times a\right)$$
48	38 39 40	3syl	$$⊢J{Isom}_{\mathrm{E},Q}\left(\mathrm{dom}J,a\times a\right)\to J^{-1}:a\times a\underset{1-1}{⟶}\mathrm{dom}J$$
49		cnvimass	$$⊢Q^{-1}\left[\left\{w\right\}\right]\subseteq \mathrm{dom}Q$$
50		inss2	$$⊢R\cap \left(\left(a\times a\right)\times \left(a\times a\right)\right)\subseteq \left(a\times a\right)\times \left(a\times a\right)$$
51	3 50	eqsstri	$$⊢Q\subseteq \left(a\times a\right)\times \left(a\times a\right)$$
52		dmss	$$⊢Q\subseteq \left(a\times a\right)\times \left(a\times a\right)\to \mathrm{dom}Q\subseteq \mathrm{dom}\left(\left(a\times a\right)\times \left(a\times a\right)\right)$$
53	51 52	ax-mp	$$⊢\mathrm{dom}Q\subseteq \mathrm{dom}\left(\left(a\times a\right)\times \left(a\times a\right)\right)$$
54		dmxpid	$$⊢\mathrm{dom}\left(\left(a\times a\right)\times \left(a\times a\right)\right)=a\times a$$
55	53 54	sseqtri	$$⊢\mathrm{dom}Q\subseteq a\times a$$
56	49 55	sstri	$$⊢Q^{-1}\left[\left\{w\right\}\right]\subseteq a\times a$$
57		f1ores	$$⊢\left(J^{-1}:a\times a\underset{1-1}{⟶}\mathrm{dom}J\wedge Q^{-1}\left[\left\{w\right\}\right]\subseteq a\times a\right)\to \left({J^{-1}\upharpoonright }_{Q^{-1}\left[\left\{w\right\}\right]}\right):Q^{-1}\left[\left\{w\right\}\right]\underset{1-1\; onto}{⟶}{J}^{-1}\left[Q^{-1}\left[\left\{w\right\}\right]\right]$$
58	48 56 57	sylancl	$$⊢J{Isom}_{\mathrm{E},Q}\left(\mathrm{dom}J,a\times a\right)\to \left({J^{-1}\upharpoonright }_{Q^{-1}\left[\left\{w\right\}\right]}\right):Q^{-1}\left[\left\{w\right\}\right]\underset{1-1\; onto}{⟶}{J}^{-1}\left[Q^{-1}\left[\left\{w\right\}\right]\right]$$
59	20 20	xpex	$$⊢\left(a\times a\right)\times \left(a\times a\right)\in \mathrm{V}$$
60	59	inex2	$$⊢R\cap \left(\left(a\times a\right)\times \left(a\times a\right)\right)\in \mathrm{V}$$
61	3 60	eqeltri	$$⊢Q\in \mathrm{V}$$
62	61	cnvex	$$⊢Q^{-1}\in \mathrm{V}$$
63	62	imaex	$$⊢Q^{-1}\left[\left\{w\right\}\right]\in \mathrm{V}$$
64	63	f1oen	$$⊢\left({J^{-1}\upharpoonright }_{Q^{-1}\left[\left\{w\right\}\right]}\right):Q^{-1}\left[\left\{w\right\}\right]\underset{1-1\; onto}{⟶}{J}^{-1}\left[Q^{-1}\left[\left\{w\right\}\right]\right]\to Q^{-1}\left[\left\{w\right\}\right]\approx J^{-1}\left[Q^{-1}\left[\left\{w\right\}\right]\right]$$
65	47 58 64	3syl	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to Q^{-1}\left[\left\{w\right\}\right]\approx J^{-1}\left[Q^{-1}\left[\left\{w\right\}\right]\right]$$
66		sseqin2	$$⊢Q^{-1}\left[\left\{w\right\}\right]\subseteq a\times a\leftrightarrow \left(a\times a\right)\cap Q^{-1}\left[\left\{w\right\}\right]=Q^{-1}\left[\left\{w\right\}\right]$$
67	56 66	mpbi	$$⊢\left(a\times a\right)\cap Q^{-1}\left[\left\{w\right\}\right]=Q^{-1}\left[\left\{w\right\}\right]$$
68	67	imaeq2i	$$⊢J^{-1}\left[\left(a\times a\right)\cap Q^{-1}\left[\left\{w\right\}\right]\right]=J^{-1}\left[Q^{-1}\left[\left\{w\right\}\right]\right]$$
69		isocnv	$$⊢J{Isom}_{\mathrm{E},Q}\left(\mathrm{dom}J,a\times a\right)\to J^{-1}{Isom}_{Q,\mathrm{E}}\left(a\times a,\mathrm{dom}J\right)$$
70	47 69	syl	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to J^{-1}{Isom}_{Q,\mathrm{E}}\left(a\times a,\mathrm{dom}J\right)$$
71		simpr	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to w\in \left(a\times a\right)$$
72		isoini	$$⊢\left(J^{-1}{Isom}_{Q,\mathrm{E}}\left(a\times a,\mathrm{dom}J\right)\wedge w\in \left(a\times a\right)\right)\to J^{-1}\left[\left(a\times a\right)\cap Q^{-1}\left[\left\{w\right\}\right]\right]=\mathrm{dom}J\cap {\mathrm{E}}^{-1}\left[\left\{J^{-1}\left(w\right)\right\}\right]$$
73	70 71 72	syl2anc	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to J^{-1}\left[\left(a\times a\right)\cap Q^{-1}\left[\left\{w\right\}\right]\right]=\mathrm{dom}J\cap {\mathrm{E}}^{-1}\left[\left\{J^{-1}\left(w\right)\right\}\right]$$
74		fvex	$$⊢J^{-1}\left(w\right)\in \mathrm{V}$$
75	74	epini	$$⊢{\mathrm{E}}^{-1}\left[\left\{J^{-1}\left(w\right)\right\}\right]=J^{-1}\left(w\right)$$
76	75	ineq2i	$$⊢\mathrm{dom}J\cap {\mathrm{E}}^{-1}\left[\left\{J^{-1}\left(w\right)\right\}\right]=\mathrm{dom}J\cap J^{-1}\left(w\right)$$
77	6	oicl	$$⊢\mathrm{Ord}\mathrm{dom}J$$
78		f1of	$$⊢J^{-1}:a\times a\underset{1-1\; onto}{⟶}\mathrm{dom}J\to J^{-1}:a\times a⟶\mathrm{dom}J$$
79	37 38 39 78	4syl	$$⊢\phi \to J^{-1}:a\times a⟶\mathrm{dom}J$$
80	79	ffvelcdmda	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to J^{-1}\left(w\right)\in \mathrm{dom}J$$
81		ordelss	$$⊢\left(\mathrm{Ord}\mathrm{dom}J\wedge J^{-1}\left(w\right)\in \mathrm{dom}J\right)\to J^{-1}\left(w\right)\subseteq \mathrm{dom}J$$
82	77 80 81	sylancr	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to J^{-1}\left(w\right)\subseteq \mathrm{dom}J$$
83		sseqin2	$$⊢J^{-1}\left(w\right)\subseteq \mathrm{dom}J\leftrightarrow \mathrm{dom}J\cap J^{-1}\left(w\right)=J^{-1}\left(w\right)$$
84	82 83	sylib	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \mathrm{dom}J\cap J^{-1}\left(w\right)=J^{-1}\left(w\right)$$
85	76 84	eqtrid	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \mathrm{dom}J\cap {\mathrm{E}}^{-1}\left[\left\{J^{-1}\left(w\right)\right\}\right]=J^{-1}\left(w\right)$$
86	73 85	eqtrd	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to J^{-1}\left[\left(a\times a\right)\cap Q^{-1}\left[\left\{w\right\}\right]\right]=J^{-1}\left(w\right)$$
87	68 86	eqtr3id	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to J^{-1}\left[Q^{-1}\left[\left\{w\right\}\right]\right]=J^{-1}\left(w\right)$$
88	65 87	breqtrd	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to Q^{-1}\left[\left\{w\right\}\right]\approx J^{-1}\left(w\right)$$
89	88	ensymd	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to J^{-1}\left(w\right)\approx Q^{-1}\left[\left\{w\right\}\right]$$
90		fvex	$$⊢1^{st}\left(w\right)\in \mathrm{V}$$
91		fvex	$$⊢2^{nd}\left(w\right)\in \mathrm{V}$$
92	90 91	unex	$$⊢1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\in \mathrm{V}$$
93	5 92	eqeltri	$$⊢M\in \mathrm{V}$$
94	93	sucex	$$⊢\mathrm{suc}M\in \mathrm{V}$$
95	94 94	xpex	$$⊢\mathrm{suc}M\times \mathrm{suc}M\in \mathrm{V}$$
96		xpss	$$⊢a\times a\subseteq \mathrm{V}\times \mathrm{V}$$
97		simp3	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\wedge z\in Q^{-1}\left[\left\{w\right\}\right]\right)\to z\in Q^{-1}\left[\left\{w\right\}\right]$$
98		vex	$$⊢z\in \mathrm{V}$$
99	98	eliniseg	$$⊢w\in \mathrm{V}\to \left(z\in Q^{-1}\left[\left\{w\right\}\right]\leftrightarrow zQw\right)$$
100	99	elv	$$⊢z\in Q^{-1}\left[\left\{w\right\}\right]\leftrightarrow zQw$$
101	97 100	sylib	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\wedge z\in Q^{-1}\left[\left\{w\right\}\right]\right)\to zQw$$
102	3	breqi	$$⊢zQw\leftrightarrow z\left(R\cap \left(\left(a\times a\right)\times \left(a\times a\right)\right)\right)w$$
103		brin	$$⊢z\left(R\cap \left(\left(a\times a\right)\times \left(a\times a\right)\right)\right)w\leftrightarrow \left(zRw\wedge z\left(\left(a\times a\right)\times \left(a\times a\right)\right)w\right)$$
104	102 103	bitri	$$⊢zQw\leftrightarrow \left(zRw\wedge z\left(\left(a\times a\right)\times \left(a\times a\right)\right)w\right)$$
105	104	simprbi	$$⊢zQw\to z\left(\left(a\times a\right)\times \left(a\times a\right)\right)w$$
106		brxp	$$⊢z\left(\left(a\times a\right)\times \left(a\times a\right)\right)w\leftrightarrow \left(z\in \left(a\times a\right)\wedge w\in \left(a\times a\right)\right)$$
107	106	simplbi	$$⊢z\left(\left(a\times a\right)\times \left(a\times a\right)\right)w\to z\in \left(a\times a\right)$$
108	101 105 107	3syl	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\wedge z\in Q^{-1}\left[\left\{w\right\}\right]\right)\to z\in \left(a\times a\right)$$
109	96 108	sselid	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\wedge z\in Q^{-1}\left[\left\{w\right\}\right]\right)\to z\in \left(\mathrm{V}\times \mathrm{V}\right)$$
110	22	adantr	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to a\in \mathrm{On}$$
111	110	3adant3	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\wedge z\in Q^{-1}\left[\left\{w\right\}\right]\right)\to a\in \mathrm{On}$$
112		xp1st	$$⊢z\in \left(a\times a\right)\to 1^{st}\left(z\right)\in a$$
113		onelon	$$⊢\left(a\in \mathrm{On}\wedge 1^{st}\left(z\right)\in a\right)\to 1^{st}\left(z\right)\in \mathrm{On}$$
114	112 113	sylan2	$$⊢\left(a\in \mathrm{On}\wedge z\in \left(a\times a\right)\right)\to 1^{st}\left(z\right)\in \mathrm{On}$$
115	111 108 114	syl2anc	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\wedge z\in Q^{-1}\left[\left\{w\right\}\right]\right)\to 1^{st}\left(z\right)\in \mathrm{On}$$
116		eloni	$$⊢a\in \mathrm{On}\to \mathrm{Ord}a$$
117		elxp7	$$⊢w\in \left(a\times a\right)\leftrightarrow \left(w\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(1^{st}\left(w\right)\in a\wedge 2^{nd}\left(w\right)\in a\right)\right)$$
118	117	simprbi	$$⊢w\in \left(a\times a\right)\to \left(1^{st}\left(w\right)\in a\wedge 2^{nd}\left(w\right)\in a\right)$$
119		ordunel	$$⊢\left(\mathrm{Ord}a\wedge 1^{st}\left(w\right)\in a\wedge 2^{nd}\left(w\right)\in a\right)\to 1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\in a$$
120	119	3expib	$$⊢\mathrm{Ord}a\to \left(\left(1^{st}\left(w\right)\in a\wedge 2^{nd}\left(w\right)\in a\right)\to 1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\in a\right)$$
121	116 118 120	syl2im	$$⊢a\in \mathrm{On}\to \left(w\in \left(a\times a\right)\to 1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\in a\right)$$
122	110 71 121	sylc	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to 1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\in a$$
123	5 122	eqeltrid	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to M\in a$$
124		simprr	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \forall m\in am\prec a\right)\right)\to \forall m\in am\prec a$$
125	4 124	sylbi	$$⊢\phi \to \forall m\in am\prec a$$
126		simprl	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \forall m\in am\prec a\right)\right)\to \mathrm{\omega }\subseteq a$$
127	4 126	sylbi	$$⊢\phi \to \mathrm{\omega }\subseteq a$$
128		iscard	$$⊢\mathrm{card}\left(a\right)=a\leftrightarrow \left(a\in \mathrm{On}\wedge \forall m\in am\prec a\right)$$
129		cardlim	$$⊢\mathrm{\omega }\subseteq \mathrm{card}\left(a\right)\leftrightarrow \mathrm{Lim}\mathrm{card}\left(a\right)$$
130		sseq2	$$⊢\mathrm{card}\left(a\right)=a\to \left(\mathrm{\omega }\subseteq \mathrm{card}\left(a\right)\leftrightarrow \mathrm{\omega }\subseteq a\right)$$
131		limeq	$$⊢\mathrm{card}\left(a\right)=a\to \left(\mathrm{Lim}\mathrm{card}\left(a\right)\leftrightarrow \mathrm{Lim}a\right)$$
132	130 131	bibi12d	$$⊢\mathrm{card}\left(a\right)=a\to \left(\left(\mathrm{\omega }\subseteq \mathrm{card}\left(a\right)\leftrightarrow \mathrm{Lim}\mathrm{card}\left(a\right)\right)\leftrightarrow \left(\mathrm{\omega }\subseteq a\leftrightarrow \mathrm{Lim}a\right)\right)$$
133	129 132	mpbii	$$⊢\mathrm{card}\left(a\right)=a\to \left(\mathrm{\omega }\subseteq a\leftrightarrow \mathrm{Lim}a\right)$$
134	128 133	sylbir	$$⊢\left(a\in \mathrm{On}\wedge \forall m\in am\prec a\right)\to \left(\mathrm{\omega }\subseteq a\leftrightarrow \mathrm{Lim}a\right)$$
135	134	biimpa	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in am\prec a\right)\wedge \mathrm{\omega }\subseteq a\right)\to \mathrm{Lim}a$$
136	22 125 127 135	syl21anc	$$⊢\phi \to \mathrm{Lim}a$$
137	136	adantr	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \mathrm{Lim}a$$
138		limsuc	$$⊢\mathrm{Lim}a\to \left(M\in a\leftrightarrow \mathrm{suc}M\in a\right)$$
139	137 138	syl	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \left(M\in a\leftrightarrow \mathrm{suc}M\in a\right)$$
140	123 139	mpbid	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \mathrm{suc}M\in a$$
141		onelon	$$⊢\left(a\in \mathrm{On}\wedge \mathrm{suc}M\in a\right)\to \mathrm{suc}M\in \mathrm{On}$$
142	22 140 141	syl2an2r	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \mathrm{suc}M\in \mathrm{On}$$
143	142	3adant3	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\wedge z\in Q^{-1}\left[\left\{w\right\}\right]\right)\to \mathrm{suc}M\in \mathrm{On}$$
144		ssun1	$$⊢1^{st}\left(z\right)\subseteq 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)$$
145	144	a1i	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\wedge z\in Q^{-1}\left[\left\{w\right\}\right]\right)\to 1^{st}\left(z\right)\subseteq 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)$$
146	104	simplbi	$$⊢zQw\to zRw$$
147		df-br	$$⊢zRw\leftrightarrow ⟨z,w⟩\in R$$
148	2	eleq2i	$$⊢⟨z,w⟩\in R\leftrightarrow ⟨z,w⟩\in \left\{⟨z,w⟩|\left(\left(z\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge w\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \left(1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)\vee \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\wedge zLw\right)\right)\right)\right\}$$
149		opabidw	$$⊢⟨z,w⟩\in \left\{⟨z,w⟩|\left(\left(z\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge w\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \left(1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)\vee \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\wedge zLw\right)\right)\right)\right\}\leftrightarrow \left(\left(z\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge w\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \left(1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)\vee \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\wedge zLw\right)\right)\right)$$
150	147 148 149	3bitri	$$⊢zRw\leftrightarrow \left(\left(z\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge w\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \left(1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)\vee \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\wedge zLw\right)\right)\right)$$
151	150	simprbi	$$⊢zRw\to \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \left(1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)\vee \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\wedge zLw\right)\right)$$
152		simpl	$$⊢\left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\wedge zLw\right)\to 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)$$
153	152	orim2i	$$⊢\left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \left(1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)\vee \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\wedge zLw\right)\right)\to \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \left(1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)\vee 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)$$
154	151 153	syl	$$⊢zRw\to \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \left(1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)\vee 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)$$
155		fvex	$$⊢1^{st}\left(z\right)\in \mathrm{V}$$
156		fvex	$$⊢2^{nd}\left(z\right)\in \mathrm{V}$$
157	155 156	unex	$$⊢1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \mathrm{V}$$
158	157	elsuc	$$⊢1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \mathrm{suc}\left(1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)\leftrightarrow \left(1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \left(1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)\vee 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)$$
159	154 158	sylibr	$$⊢zRw\to 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \mathrm{suc}\left(1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)$$
160		suceq	$$⊢M=1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\to \mathrm{suc}M=\mathrm{suc}\left(1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)$$
161	5 160	ax-mp	$$⊢\mathrm{suc}M=\mathrm{suc}\left(1^{st}\left(w\right)\cup 2^{nd}\left(w\right)\right)$$
162	159 161	eleqtrrdi	$$⊢zRw\to 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \mathrm{suc}M$$
163	101 146 162	3syl	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\wedge z\in Q^{-1}\left[\left\{w\right\}\right]\right)\to 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \mathrm{suc}M$$
164		ontr2	$$⊢\left(1^{st}\left(z\right)\in \mathrm{On}\wedge \mathrm{suc}M\in \mathrm{On}\right)\to \left(\left(1^{st}\left(z\right)\subseteq 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\wedge 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \mathrm{suc}M\right)\to 1^{st}\left(z\right)\in \mathrm{suc}M\right)$$
165	164	imp	$$⊢\left(\left(1^{st}\left(z\right)\in \mathrm{On}\wedge \mathrm{suc}M\in \mathrm{On}\right)\wedge \left(1^{st}\left(z\right)\subseteq 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\wedge 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \mathrm{suc}M\right)\right)\to 1^{st}\left(z\right)\in \mathrm{suc}M$$
166	115 143 145 163 165	syl22anc	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\wedge z\in Q^{-1}\left[\left\{w\right\}\right]\right)\to 1^{st}\left(z\right)\in \mathrm{suc}M$$
167		xp2nd	$$⊢z\in \left(a\times a\right)\to 2^{nd}\left(z\right)\in a$$
168		onelon	$$⊢\left(a\in \mathrm{On}\wedge 2^{nd}\left(z\right)\in a\right)\to 2^{nd}\left(z\right)\in \mathrm{On}$$
169	167 168	sylan2	$$⊢\left(a\in \mathrm{On}\wedge z\in \left(a\times a\right)\right)\to 2^{nd}\left(z\right)\in \mathrm{On}$$
170	111 108 169	syl2anc	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\wedge z\in Q^{-1}\left[\left\{w\right\}\right]\right)\to 2^{nd}\left(z\right)\in \mathrm{On}$$
171		ssun2	$$⊢2^{nd}\left(z\right)\subseteq 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)$$
172	171	a1i	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\wedge z\in Q^{-1}\left[\left\{w\right\}\right]\right)\to 2^{nd}\left(z\right)\subseteq 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)$$
173		ontr2	$$⊢\left(2^{nd}\left(z\right)\in \mathrm{On}\wedge \mathrm{suc}M\in \mathrm{On}\right)\to \left(\left(2^{nd}\left(z\right)\subseteq 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\wedge 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \mathrm{suc}M\right)\to 2^{nd}\left(z\right)\in \mathrm{suc}M\right)$$
174	173	imp	$$⊢\left(\left(2^{nd}\left(z\right)\in \mathrm{On}\wedge \mathrm{suc}M\in \mathrm{On}\right)\wedge \left(2^{nd}\left(z\right)\subseteq 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\wedge 1^{st}\left(z\right)\cup 2^{nd}\left(z\right)\in \mathrm{suc}M\right)\right)\to 2^{nd}\left(z\right)\in \mathrm{suc}M$$
175	170 143 172 163 174	syl22anc	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\wedge z\in Q^{-1}\left[\left\{w\right\}\right]\right)\to 2^{nd}\left(z\right)\in \mathrm{suc}M$$
176		elxp7	$$⊢z\in \left(\mathrm{suc}M\times \mathrm{suc}M\right)\leftrightarrow \left(z\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(1^{st}\left(z\right)\in \mathrm{suc}M\wedge 2^{nd}\left(z\right)\in \mathrm{suc}M\right)\right)$$
177	176	biimpri	$$⊢\left(z\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(1^{st}\left(z\right)\in \mathrm{suc}M\wedge 2^{nd}\left(z\right)\in \mathrm{suc}M\right)\right)\to z\in \left(\mathrm{suc}M\times \mathrm{suc}M\right)$$
178	109 166 175 177	syl12anc	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\wedge z\in Q^{-1}\left[\left\{w\right\}\right]\right)\to z\in \left(\mathrm{suc}M\times \mathrm{suc}M\right)$$
179	178	3expia	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \left(z\in Q^{-1}\left[\left\{w\right\}\right]\to z\in \left(\mathrm{suc}M\times \mathrm{suc}M\right)\right)$$
180	179	ssrdv	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to Q^{-1}\left[\left\{w\right\}\right]\subseteq \mathrm{suc}M\times \mathrm{suc}M$$
181		ssdomg	$$⊢\mathrm{suc}M\times \mathrm{suc}M\in \mathrm{V}\to \left(Q^{-1}\left[\left\{w\right\}\right]\subseteq \mathrm{suc}M\times \mathrm{suc}M\to Q^{-1}\left[\left\{w\right\}\right]\preccurlyeq \left(\mathrm{suc}M\times \mathrm{suc}M\right)\right)$$
182	95 180 181	mpsyl	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to Q^{-1}\left[\left\{w\right\}\right]\preccurlyeq \left(\mathrm{suc}M\times \mathrm{suc}M\right)$$
183	127	adantr	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \mathrm{\omega }\subseteq a$$
184		nnfi	$$⊢\mathrm{suc}M\in \mathrm{\omega }\to \mathrm{suc}M\in \mathrm{Fin}$$
185		xpfi	$$⊢\left(\mathrm{suc}M\in \mathrm{Fin}\wedge \mathrm{suc}M\in \mathrm{Fin}\right)\to \mathrm{suc}M\times \mathrm{suc}M\in \mathrm{Fin}$$
186	185	anidms	$$⊢\mathrm{suc}M\in \mathrm{Fin}\to \mathrm{suc}M\times \mathrm{suc}M\in \mathrm{Fin}$$
187		isfinite	$$⊢\mathrm{suc}M\times \mathrm{suc}M\in \mathrm{Fin}\leftrightarrow \left(\mathrm{suc}M\times \mathrm{suc}M\right)\prec \mathrm{\omega }$$
188	186 187	sylib	$$⊢\mathrm{suc}M\in \mathrm{Fin}\to \left(\mathrm{suc}M\times \mathrm{suc}M\right)\prec \mathrm{\omega }$$
189	184 188	syl	$$⊢\mathrm{suc}M\in \mathrm{\omega }\to \left(\mathrm{suc}M\times \mathrm{suc}M\right)\prec \mathrm{\omega }$$
190		ssdomg	$$⊢a\in \mathrm{V}\to \left(\mathrm{\omega }\subseteq a\to \mathrm{\omega }\preccurlyeq a\right)$$
191	190	elv	$$⊢\mathrm{\omega }\subseteq a\to \mathrm{\omega }\preccurlyeq a$$
192		sdomdomtr	$$⊢\left(\left(\mathrm{suc}M\times \mathrm{suc}M\right)\prec \mathrm{\omega }\wedge \mathrm{\omega }\preccurlyeq a\right)\to \left(\mathrm{suc}M\times \mathrm{suc}M\right)\prec a$$
193	189 191 192	syl2an	$$⊢\left(\mathrm{suc}M\in \mathrm{\omega }\wedge \mathrm{\omega }\subseteq a\right)\to \left(\mathrm{suc}M\times \mathrm{suc}M\right)\prec a$$
194	193	expcom	$$⊢\mathrm{\omega }\subseteq a\to \left(\mathrm{suc}M\in \mathrm{\omega }\to \left(\mathrm{suc}M\times \mathrm{suc}M\right)\prec a\right)$$
195	183 194	syl	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \left(\mathrm{suc}M\in \mathrm{\omega }\to \left(\mathrm{suc}M\times \mathrm{suc}M\right)\prec a\right)$$
196		breq1	$$⊢m=\mathrm{suc}M\to \left(m\prec a\leftrightarrow \mathrm{suc}M\prec a\right)$$
197	125	adantr	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \forall m\in am\prec a$$
198	196 197 140	rspcdva	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \mathrm{suc}M\prec a$$
199		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
200		ontri1	$$⊢\left(\mathrm{\omega }\in \mathrm{On}\wedge \mathrm{suc}M\in \mathrm{On}\right)\to \left(\mathrm{\omega }\subseteq \mathrm{suc}M\leftrightarrow \neg \mathrm{suc}M\in \mathrm{\omega }\right)$$
201	199 142 200	sylancr	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \left(\mathrm{\omega }\subseteq \mathrm{suc}M\leftrightarrow \neg \mathrm{suc}M\in \mathrm{\omega }\right)$$
202		sseq2	$$⊢m=\mathrm{suc}M\to \left(\mathrm{\omega }\subseteq m\leftrightarrow \mathrm{\omega }\subseteq \mathrm{suc}M\right)$$
203		xpeq12	$$⊢\left(m=\mathrm{suc}M\wedge m=\mathrm{suc}M\right)\to m\times m=\mathrm{suc}M\times \mathrm{suc}M$$
204	203	anidms	$$⊢m=\mathrm{suc}M\to m\times m=\mathrm{suc}M\times \mathrm{suc}M$$
205		id	$$⊢m=\mathrm{suc}M\to m=\mathrm{suc}M$$
206	204 205	breq12d	$$⊢m=\mathrm{suc}M\to \left(\left(m\times m\right)\approx m\leftrightarrow \left(\mathrm{suc}M\times \mathrm{suc}M\right)\approx \mathrm{suc}M\right)$$
207	202 206	imbi12d	$$⊢m=\mathrm{suc}M\to \left(\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\leftrightarrow \left(\mathrm{\omega }\subseteq \mathrm{suc}M\to \left(\mathrm{suc}M\times \mathrm{suc}M\right)\approx \mathrm{suc}M\right)\right)$$
208		simplr	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \forall m\in am\prec a\right)\right)\to \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)$$
209	4 208	sylbi	$$⊢\phi \to \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)$$
210	209	adantr	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)$$
211	207 210 140	rspcdva	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \left(\mathrm{\omega }\subseteq \mathrm{suc}M\to \left(\mathrm{suc}M\times \mathrm{suc}M\right)\approx \mathrm{suc}M\right)$$
212	201 211	sylbird	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \left(\neg \mathrm{suc}M\in \mathrm{\omega }\to \left(\mathrm{suc}M\times \mathrm{suc}M\right)\approx \mathrm{suc}M\right)$$
213		ensdomtr	$$⊢\left(\left(\mathrm{suc}M\times \mathrm{suc}M\right)\approx \mathrm{suc}M\wedge \mathrm{suc}M\prec a\right)\to \left(\mathrm{suc}M\times \mathrm{suc}M\right)\prec a$$
214	213	expcom	$$⊢\mathrm{suc}M\prec a\to \left(\left(\mathrm{suc}M\times \mathrm{suc}M\right)\approx \mathrm{suc}M\to \left(\mathrm{suc}M\times \mathrm{suc}M\right)\prec a\right)$$
215	198 212 214	sylsyld	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \left(\neg \mathrm{suc}M\in \mathrm{\omega }\to \left(\mathrm{suc}M\times \mathrm{suc}M\right)\prec a\right)$$
216	195 215	pm2.61d	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \left(\mathrm{suc}M\times \mathrm{suc}M\right)\prec a$$
217		domsdomtr	$$⊢\left(Q^{-1}\left[\left\{w\right\}\right]\preccurlyeq \left(\mathrm{suc}M\times \mathrm{suc}M\right)\wedge \left(\mathrm{suc}M\times \mathrm{suc}M\right)\prec a\right)\to Q^{-1}\left[\left\{w\right\}\right]\prec a$$
218	182 216 217	syl2anc	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to Q^{-1}\left[\left\{w\right\}\right]\prec a$$
219		ensdomtr	$$⊢\left(J^{-1}\left(w\right)\approx Q^{-1}\left[\left\{w\right\}\right]\wedge Q^{-1}\left[\left\{w\right\}\right]\prec a\right)\to J^{-1}\left(w\right)\prec a$$
220	89 218 219	syl2anc	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to J^{-1}\left(w\right)\prec a$$
221		ordelon	$$⊢\left(\mathrm{Ord}\mathrm{dom}J\wedge J^{-1}\left(w\right)\in \mathrm{dom}J\right)\to J^{-1}\left(w\right)\in \mathrm{On}$$
222	77 80 221	sylancr	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to J^{-1}\left(w\right)\in \mathrm{On}$$
223		onenon	$$⊢a\in \mathrm{On}\to a\in \mathrm{dom}\mathrm{card}$$
224	110 223	syl	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to a\in \mathrm{dom}\mathrm{card}$$
225		cardsdomel	$$⊢\left(J^{-1}\left(w\right)\in \mathrm{On}\wedge a\in \mathrm{dom}\mathrm{card}\right)\to \left(J^{-1}\left(w\right)\prec a\leftrightarrow J^{-1}\left(w\right)\in \mathrm{card}\left(a\right)\right)$$
226	222 224 225	syl2anc	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \left(J^{-1}\left(w\right)\prec a\leftrightarrow J^{-1}\left(w\right)\in \mathrm{card}\left(a\right)\right)$$
227	220 226	mpbid	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to J^{-1}\left(w\right)\in \mathrm{card}\left(a\right)$$
228		eleq2	$$⊢\mathrm{card}\left(a\right)=a\to \left(J^{-1}\left(w\right)\in \mathrm{card}\left(a\right)\leftrightarrow J^{-1}\left(w\right)\in a\right)$$
229	128 228	sylbir	$$⊢\left(a\in \mathrm{On}\wedge \forall m\in am\prec a\right)\to \left(J^{-1}\left(w\right)\in \mathrm{card}\left(a\right)\leftrightarrow J^{-1}\left(w\right)\in a\right)$$
230	22 197 229	syl2an2r	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to \left(J^{-1}\left(w\right)\in \mathrm{card}\left(a\right)\leftrightarrow J^{-1}\left(w\right)\in a\right)$$
231	227 230	mpbid	$$⊢\left(\phi \wedge w\in \left(a\times a\right)\right)\to J^{-1}\left(w\right)\in a$$
232	231	ralrimiva	$$⊢\phi \to \forall w\in \left(a\times a\right)J^{-1}\left(w\right)\in a$$
233		fnfvrnss	$$⊢\left(J^{-1}Fn\left(a\times a\right)\wedge \forall w\in \left(a\times a\right)J^{-1}\left(w\right)\in a\right)\to \mathrm{ran}{J}^{-1}\subseteq a$$
234		ssdomg	$$⊢a\in \mathrm{V}\to \left(\mathrm{ran}{J}^{-1}\subseteq a\to \mathrm{ran}{J}^{-1}\preccurlyeq a\right)$$
235	19 233 234	mpsyl	$$⊢\left(J^{-1}Fn\left(a\times a\right)\wedge \forall w\in \left(a\times a\right)J^{-1}\left(w\right)\in a\right)\to \mathrm{ran}{J}^{-1}\preccurlyeq a$$
236	46 232 235	syl2anc	$$⊢\phi \to \mathrm{ran}{J}^{-1}\preccurlyeq a$$
237		endomtr	$$⊢\left(\left(a\times a\right)\approx \mathrm{ran}{J}^{-1}\wedge \mathrm{ran}{J}^{-1}\preccurlyeq a\right)\to \left(a\times a\right)\preccurlyeq a$$
238	44 236 237	syl2anc	$$⊢\phi \to \left(a\times a\right)\preccurlyeq a$$
239	4 238	sylbir	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \forall m\in am\prec a\right)\right)\to \left(a\times a\right)\preccurlyeq a$$
240		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
241		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
242	240 241	eqeltrri	$$⊢\left\{\varnothing \right\}\in \mathrm{\omega }$$
243		nnsdom	$$⊢\left\{\varnothing \right\}\in \mathrm{\omega }\to \left\{\varnothing \right\}\prec \mathrm{\omega }$$
244		sdomdom	$$⊢\left\{\varnothing \right\}\prec \mathrm{\omega }\to \left\{\varnothing \right\}\preccurlyeq \mathrm{\omega }$$
245	242 243 244	mp2b	$$⊢\left\{\varnothing \right\}\preccurlyeq \mathrm{\omega }$$
246		domtr	$$⊢\left(\left\{\varnothing \right\}\preccurlyeq \mathrm{\omega }\wedge \mathrm{\omega }\preccurlyeq a\right)\to \left\{\varnothing \right\}\preccurlyeq a$$
247	245 191 246	sylancr	$$⊢\mathrm{\omega }\subseteq a\to \left\{\varnothing \right\}\preccurlyeq a$$
248		0ex	$$⊢\varnothing \in \mathrm{V}$$
249	19 248	xpsnen	$$⊢\left(a\times \left\{\varnothing \right\}\right)\approx a$$
250	249	ensymi	$$⊢a\approx \left(a\times \left\{\varnothing \right\}\right)$$
251	19	xpdom2	$$⊢\left\{\varnothing \right\}\preccurlyeq a\to \left(a\times \left\{\varnothing \right\}\right)\preccurlyeq \left(a\times a\right)$$
252		endomtr	$$⊢\left(a\approx \left(a\times \left\{\varnothing \right\}\right)\wedge \left(a\times \left\{\varnothing \right\}\right)\preccurlyeq \left(a\times a\right)\right)\to a\preccurlyeq \left(a\times a\right)$$
253	250 251 252	sylancr	$$⊢\left\{\varnothing \right\}\preccurlyeq a\to a\preccurlyeq \left(a\times a\right)$$
254	247 253	syl	$$⊢\mathrm{\omega }\subseteq a\to a\preccurlyeq \left(a\times a\right)$$
255	254	ad2antrl	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \forall m\in am\prec a\right)\right)\to a\preccurlyeq \left(a\times a\right)$$
256		sbth	$$⊢\left(\left(a\times a\right)\preccurlyeq a\wedge a\preccurlyeq \left(a\times a\right)\right)\to \left(a\times a\right)\approx a$$
257	239 255 256	syl2anc	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \forall m\in am\prec a\right)\right)\to \left(a\times a\right)\approx a$$
258	257	expr	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \mathrm{\omega }\subseteq a\right)\to \left(\forall m\in am\prec a\to \left(a\times a\right)\approx a\right)$$
259		simplr	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \neg \forall m\in am\prec a\right)\right)\to \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)$$
260		simpll	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \neg \forall m\in am\prec a\right)\right)\to a\in \mathrm{On}$$
261		simprr	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \neg \forall m\in am\prec a\right)\right)\to \neg \forall m\in am\prec a$$
262		rexnal	$$⊢\exists m\in a\neg m\prec a\leftrightarrow \neg \forall m\in am\prec a$$
263		onelss	$$⊢a\in \mathrm{On}\to \left(m\in a\to m\subseteq a\right)$$
264		ssdomg	$$⊢a\in \mathrm{On}\to \left(m\subseteq a\to m\preccurlyeq a\right)$$
265	263 264	syld	$$⊢a\in \mathrm{On}\to \left(m\in a\to m\preccurlyeq a\right)$$
266		bren2	$$⊢m\approx a\leftrightarrow \left(m\preccurlyeq a\wedge \neg m\prec a\right)$$
267	266	simplbi2	$$⊢m\preccurlyeq a\to \left(\neg m\prec a\to m\approx a\right)$$
268	265 267	syl6	$$⊢a\in \mathrm{On}\to \left(m\in a\to \left(\neg m\prec a\to m\approx a\right)\right)$$
269	268	reximdvai	$$⊢a\in \mathrm{On}\to \left(\exists m\in a\neg m\prec a\to \exists m\in am\approx a\right)$$
270	262 269	biimtrrid	$$⊢a\in \mathrm{On}\to \left(\neg \forall m\in am\prec a\to \exists m\in am\approx a\right)$$
271	260 261 270	sylc	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \neg \forall m\in am\prec a\right)\right)\to \exists m\in am\approx a$$
272		r19.29	$$⊢\left(\forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\wedge \exists m\in am\approx a\right)\to \exists m\in a\left(\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\wedge m\approx a\right)$$
273	259 271 272	syl2anc	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \neg \forall m\in am\prec a\right)\right)\to \exists m\in a\left(\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\wedge m\approx a\right)$$
274		simprl	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \neg \forall m\in am\prec a\right)\right)\to \mathrm{\omega }\subseteq a$$
275		onelon	$$⊢\left(a\in \mathrm{On}\wedge m\in a\right)\to m\in \mathrm{On}$$
276		ensym	$$⊢m\approx a\to a\approx m$$
277		domentr	$$⊢\left(\mathrm{\omega }\preccurlyeq a\wedge a\approx m\right)\to \mathrm{\omega }\preccurlyeq m$$
278	191 276 277	syl2an	$$⊢\left(\mathrm{\omega }\subseteq a\wedge m\approx a\right)\to \mathrm{\omega }\preccurlyeq m$$
279		domnsym	$$⊢\mathrm{\omega }\preccurlyeq m\to \neg m\prec \mathrm{\omega }$$
280		nnsdom	$$⊢m\in \mathrm{\omega }\to m\prec \mathrm{\omega }$$
281	279 280	nsyl	$$⊢\mathrm{\omega }\preccurlyeq m\to \neg m\in \mathrm{\omega }$$
282		ontri1	$$⊢\left(\mathrm{\omega }\in \mathrm{On}\wedge m\in \mathrm{On}\right)\to \left(\mathrm{\omega }\subseteq m\leftrightarrow \neg m\in \mathrm{\omega }\right)$$
283	199 282	mpan	$$⊢m\in \mathrm{On}\to \left(\mathrm{\omega }\subseteq m\leftrightarrow \neg m\in \mathrm{\omega }\right)$$
284	281 283	imbitrrid	$$⊢m\in \mathrm{On}\to \left(\mathrm{\omega }\preccurlyeq m\to \mathrm{\omega }\subseteq m\right)$$
285	275 278 284	syl2im	$$⊢\left(a\in \mathrm{On}\wedge m\in a\right)\to \left(\left(\mathrm{\omega }\subseteq a\wedge m\approx a\right)\to \mathrm{\omega }\subseteq m\right)$$
286	285	expd	$$⊢\left(a\in \mathrm{On}\wedge m\in a\right)\to \left(\mathrm{\omega }\subseteq a\to \left(m\approx a\to \mathrm{\omega }\subseteq m\right)\right)$$
287	286	impcom	$$⊢\left(\mathrm{\omega }\subseteq a\wedge \left(a\in \mathrm{On}\wedge m\in a\right)\right)\to \left(m\approx a\to \mathrm{\omega }\subseteq m\right)$$
288	287	imim1d	$$⊢\left(\mathrm{\omega }\subseteq a\wedge \left(a\in \mathrm{On}\wedge m\in a\right)\right)\to \left(\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\to \left(m\approx a\to \left(m\times m\right)\approx m\right)\right)$$
289	288	imp32	$$⊢\left(\left(\mathrm{\omega }\subseteq a\wedge \left(a\in \mathrm{On}\wedge m\in a\right)\right)\wedge \left(\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\wedge m\approx a\right)\right)\to \left(m\times m\right)\approx m$$
290		entr	$$⊢\left(\left(m\times m\right)\approx m\wedge m\approx a\right)\to \left(m\times m\right)\approx a$$
291	290	ancoms	$$⊢\left(m\approx a\wedge \left(m\times m\right)\approx m\right)\to \left(m\times m\right)\approx a$$
292		xpen	$$⊢\left(a\approx m\wedge a\approx m\right)\to \left(a\times a\right)\approx \left(m\times m\right)$$
293	292	anidms	$$⊢a\approx m\to \left(a\times a\right)\approx \left(m\times m\right)$$
294		entr	$$⊢\left(\left(a\times a\right)\approx \left(m\times m\right)\wedge \left(m\times m\right)\approx a\right)\to \left(a\times a\right)\approx a$$
295	293 294	sylan	$$⊢\left(a\approx m\wedge \left(m\times m\right)\approx a\right)\to \left(a\times a\right)\approx a$$
296	276 291 295	syl2an2r	$$⊢\left(m\approx a\wedge \left(m\times m\right)\approx m\right)\to \left(a\times a\right)\approx a$$
297	296	ex	$$⊢m\approx a\to \left(\left(m\times m\right)\approx m\to \left(a\times a\right)\approx a\right)$$
298	297	ad2antll	$$⊢\left(\left(\mathrm{\omega }\subseteq a\wedge \left(a\in \mathrm{On}\wedge m\in a\right)\right)\wedge \left(\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\wedge m\approx a\right)\right)\to \left(\left(m\times m\right)\approx m\to \left(a\times a\right)\approx a\right)$$
299	289 298	mpd	$$⊢\left(\left(\mathrm{\omega }\subseteq a\wedge \left(a\in \mathrm{On}\wedge m\in a\right)\right)\wedge \left(\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\wedge m\approx a\right)\right)\to \left(a\times a\right)\approx a$$
300	299	ex	$$⊢\left(\mathrm{\omega }\subseteq a\wedge \left(a\in \mathrm{On}\wedge m\in a\right)\right)\to \left(\left(\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\wedge m\approx a\right)\to \left(a\times a\right)\approx a\right)$$
301	300	expr	$$⊢\left(\mathrm{\omega }\subseteq a\wedge a\in \mathrm{On}\right)\to \left(m\in a\to \left(\left(\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\wedge m\approx a\right)\to \left(a\times a\right)\approx a\right)\right)$$
302	301	rexlimdv	$$⊢\left(\mathrm{\omega }\subseteq a\wedge a\in \mathrm{On}\right)\to \left(\exists m\in a\left(\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\wedge m\approx a\right)\to \left(a\times a\right)\approx a\right)$$
303	274 260 302	syl2anc	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \neg \forall m\in am\prec a\right)\right)\to \left(\exists m\in a\left(\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\wedge m\approx a\right)\to \left(a\times a\right)\approx a\right)$$
304	273 303	mpd	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \left(\mathrm{\omega }\subseteq a\wedge \neg \forall m\in am\prec a\right)\right)\to \left(a\times a\right)\approx a$$
305	304	expr	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \mathrm{\omega }\subseteq a\right)\to \left(\neg \forall m\in am\prec a\to \left(a\times a\right)\approx a\right)$$
306	258 305	pm2.61d	$$⊢\left(\left(a\in \mathrm{On}\wedge \forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\right)\wedge \mathrm{\omega }\subseteq a\right)\to \left(a\times a\right)\approx a$$
307	306	exp31	$$⊢a\in \mathrm{On}\to \left(\forall m\in a\left(\mathrm{\omega }\subseteq m\to \left(m\times m\right)\approx m\right)\to \left(\mathrm{\omega }\subseteq a\to \left(a\times a\right)\approx a\right)\right)$$
308	12 18 307	tfis3	$$⊢A\in \mathrm{On}\to \left(\mathrm{\omega }\subseteq A\to \left(A\times A\right)\approx A\right)$$
309	308	imp	$$⊢\left(A\in \mathrm{On}\wedge \mathrm{\omega }\subseteq A\right)\to \left(A\times A\right)\approx A$$