Theorem canthp1lem2

Description: Lemma for canthp1 . (Contributed by Mario Carneiro, 18-May-2015)

	Ref	Expression
Hypotheses	canthp1lem2.1	$$⊢\phi \to 1_{𝑜}\prec A$$
	canthp1lem2.2	$$⊢\phi \to F:𝒫A\underset{1-1\; onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
	canthp1lem2.3	$$⊢\phi \to G:\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\setminus \left\{F\left(A\right)\right\}\underset{1-1\; onto}{⟶}A$$
	canthp1lem2.4	$$⊢H=\left(G\circ F\right)\circ \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)$$
	canthp1lem2.5	$$⊢W=\left\{⟨x,r⟩|\left(\left(x\subseteq A\wedge r\subseteq x\times x\right)\wedge \left(r\mathrm{We}x\wedge \forall y\in xH\left(r^{-1}\left[\left\{y\right\}\right]\right)=y\right)\right)\right\}$$
	canthp1lem2.6	$$⊢B=\bigcup \mathrm{dom}W$$
Assertion	canthp1lem2	$$⊢\neg \phi$$

Proof

Step	Hyp	Ref	Expression
1		canthp1lem2.1	$$⊢\phi \to 1_{𝑜}\prec A$$
2		canthp1lem2.2	$$⊢\phi \to F:𝒫A\underset{1-1\; onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
3		canthp1lem2.3	$$⊢\phi \to G:\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\setminus \left\{F\left(A\right)\right\}\underset{1-1\; onto}{⟶}A$$
4		canthp1lem2.4	$$⊢H=\left(G\circ F\right)\circ \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)$$
5		canthp1lem2.5	$$⊢W=\left\{⟨x,r⟩|\left(\left(x\subseteq A\wedge r\subseteq x\times x\right)\wedge \left(r\mathrm{We}x\wedge \forall y\in xH\left(r^{-1}\left[\left\{y\right\}\right]\right)=y\right)\right)\right\}$$
6		canthp1lem2.6	$$⊢B=\bigcup \mathrm{dom}W$$
7		relsdom	$$⊢\mathrm{Rel}\prec$$
8	7	brrelex2i	$$⊢1_{𝑜}\prec A\to A\in \mathrm{V}$$
9	1 8	syl	$$⊢\phi \to A\in \mathrm{V}$$
10	9	pwexd	$$⊢\phi \to 𝒫A\in \mathrm{V}$$
11		f1oeng	$$⊢\left(𝒫A\in \mathrm{V}\wedge F:𝒫A\underset{1-1\; onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\right)\to 𝒫A\approx \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
12	10 2 11	syl2anc	$$⊢\phi \to 𝒫A\approx \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
13	12	ensymd	$$⊢\phi \to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx 𝒫A$$
14		canth2g	$$⊢A\in \mathrm{V}\to A\prec 𝒫A$$
15	9 14	syl	$$⊢\phi \to A\prec 𝒫A$$
16		sdomen2	$$⊢𝒫A\approx \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\to \left(A\prec 𝒫A\leftrightarrow A\prec \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\right)$$
17	12 16	syl	$$⊢\phi \to \left(A\prec 𝒫A\leftrightarrow A\prec \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\right)$$
18	15 17	mpbid	$$⊢\phi \to A\prec \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
19		sdomnen	$$⊢A\prec \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\to \neg A\approx \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
20	18 19	syl	$$⊢\phi \to \neg A\approx \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
21		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
22		onenon	$$⊢\mathrm{\omega }\in \mathrm{On}\to \mathrm{\omega }\in \mathrm{dom}\mathrm{card}$$
23	21 22	ax-mp	$$⊢\mathrm{\omega }\in \mathrm{dom}\mathrm{card}$$
24		dff1o3	$$⊢F:𝒫A\underset{1-1\; onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\leftrightarrow \left(F:𝒫A\underset{onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\wedge \mathrm{Fun}{F}^{-1}\right)$$
25	24	simprbi	$$⊢F:𝒫A\underset{1-1\; onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\to \mathrm{Fun}{F}^{-1}$$
26	2 25	syl	$$⊢\phi \to \mathrm{Fun}{F}^{-1}$$
27		f1ofo	$$⊢F:𝒫A\underset{1-1\; onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\to F:𝒫A\underset{onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
28	2 27	syl	$$⊢\phi \to F:𝒫A\underset{onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
29		f1ofn	$$⊢F:𝒫A\underset{1-1\; onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\to FFn𝒫A$$
30		fnresdm	$$⊢FFn𝒫A\to {F\upharpoonright }_{𝒫A}=F$$
31		foeq1	$$⊢{F\upharpoonright }_{𝒫A}=F\to \left(\left({F\upharpoonright }_{𝒫A}\right):𝒫A\underset{onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\leftrightarrow F:𝒫A\underset{onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\right)$$
32	2 29 30 31	4syl	$$⊢\phi \to \left(\left({F\upharpoonright }_{𝒫A}\right):𝒫A\underset{onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\leftrightarrow F:𝒫A\underset{onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\right)$$
33	28 32	mpbird	$$⊢\phi \to \left({F\upharpoonright }_{𝒫A}\right):𝒫A\underset{onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
34		fvex	$$⊢F\left(A\right)\in \mathrm{V}$$
35		f1osng	$$⊢\left(A\in \mathrm{V}\wedge F\left(A\right)\in \mathrm{V}\right)\to \left\{⟨A,F\left(A\right)⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{F\left(A\right)\right\}$$
36	9 34 35	sylancl	$$⊢\phi \to \left\{⟨A,F\left(A\right)⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{F\left(A\right)\right\}$$
37	2 29	syl	$$⊢\phi \to FFn𝒫A$$
38		pwidg	$$⊢A\in \mathrm{V}\to A\in 𝒫A$$
39	9 38	syl	$$⊢\phi \to A\in 𝒫A$$
40		fnressn	$$⊢\left(FFn𝒫A\wedge A\in 𝒫A\right)\to {F\upharpoonright }_{\left\{A\right\}}=\left\{⟨A,F\left(A\right)⟩\right\}$$
41	37 39 40	syl2anc	$$⊢\phi \to {F\upharpoonright }_{\left\{A\right\}}=\left\{⟨A,F\left(A\right)⟩\right\}$$
42	41	f1oeq1d	$$⊢\phi \to \left(\left({F\upharpoonright }_{\left\{A\right\}}\right):\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{F\left(A\right)\right\}\leftrightarrow \left\{⟨A,F\left(A\right)⟩\right\}:\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{F\left(A\right)\right\}\right)$$
43	36 42	mpbird	$$⊢\phi \to \left({F\upharpoonright }_{\left\{A\right\}}\right):\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{F\left(A\right)\right\}$$
44		f1ofo	$$⊢\left({F\upharpoonright }_{\left\{A\right\}}\right):\left\{A\right\}\underset{1-1\; onto}{⟶}\left\{F\left(A\right)\right\}\to \left({F\upharpoonright }_{\left\{A\right\}}\right):\left\{A\right\}\underset{onto}{⟶}\left\{F\left(A\right)\right\}$$
45	43 44	syl	$$⊢\phi \to \left({F\upharpoonright }_{\left\{A\right\}}\right):\left\{A\right\}\underset{onto}{⟶}\left\{F\left(A\right)\right\}$$
46		resdif	$$⊢\left(\mathrm{Fun}{F}^{-1}\wedge \left({F\upharpoonright }_{𝒫A}\right):𝒫A\underset{onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\wedge \left({F\upharpoonright }_{\left\{A\right\}}\right):\left\{A\right\}\underset{onto}{⟶}\left\{F\left(A\right)\right\}\right)\to \left({F\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right):𝒫A\setminus \left\{A\right\}\underset{1-1\; onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\setminus \left\{F\left(A\right)\right\}$$
47	26 33 45 46	syl3anc	$$⊢\phi \to \left({F\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right):𝒫A\setminus \left\{A\right\}\underset{1-1\; onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\setminus \left\{F\left(A\right)\right\}$$
48		f1oco	$$⊢\left(G:\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\setminus \left\{F\left(A\right)\right\}\underset{1-1\; onto}{⟶}A\wedge \left({F\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right):𝒫A\setminus \left\{A\right\}\underset{1-1\; onto}{⟶}\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\setminus \left\{F\left(A\right)\right\}\right)\to \left(G\circ \left({F\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\right):𝒫A\setminus \left\{A\right\}\underset{1-1\; onto}{⟶}A$$
49	3 47 48	syl2anc	$$⊢\phi \to \left(G\circ \left({F\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\right):𝒫A\setminus \left\{A\right\}\underset{1-1\; onto}{⟶}A$$
50		resco	$$⊢{\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}=G\circ \left({F\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)$$
51		f1oeq1	$$⊢{\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}=G\circ \left({F\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\to \left(\left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right):𝒫A\setminus \left\{A\right\}\underset{1-1\; onto}{⟶}A\leftrightarrow \left(G\circ \left({F\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\right):𝒫A\setminus \left\{A\right\}\underset{1-1\; onto}{⟶}A\right)$$
52	50 51	ax-mp	$$⊢\left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right):𝒫A\setminus \left\{A\right\}\underset{1-1\; onto}{⟶}A\leftrightarrow \left(G\circ \left({F\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\right):𝒫A\setminus \left\{A\right\}\underset{1-1\; onto}{⟶}A$$
53	49 52	sylibr	$$⊢\phi \to \left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right):𝒫A\setminus \left\{A\right\}\underset{1-1\; onto}{⟶}A$$
54		f1of	$$⊢\left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right):𝒫A\setminus \left\{A\right\}\underset{1-1\; onto}{⟶}A\to \left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right):𝒫A\setminus \left\{A\right\}⟶A$$
55	53 54	syl	$$⊢\phi \to \left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right):𝒫A\setminus \left\{A\right\}⟶A$$
56		0elpw	$$⊢\varnothing \in 𝒫A$$
57	56	a1i	$$⊢\left(\left(\phi \wedge x\in 𝒫A\right)\wedge x=A\right)\to \varnothing \in 𝒫A$$
58		sdom0	$$⊢\neg 1_{𝑜}\prec \varnothing$$
59		breq2	$$⊢\varnothing =A\to \left(1_{𝑜}\prec \varnothing \leftrightarrow 1_{𝑜}\prec A\right)$$
60	58 59	mtbii	$$⊢\varnothing =A\to \neg 1_{𝑜}\prec A$$
61	60	necon2ai	$$⊢1_{𝑜}\prec A\to \varnothing \ne A$$
62	1 61	syl	$$⊢\phi \to \varnothing \ne A$$
63	62	ad2antrr	$$⊢\left(\left(\phi \wedge x\in 𝒫A\right)\wedge x=A\right)\to \varnothing \ne A$$
64		eldifsn	$$⊢\varnothing \in \left(𝒫A\setminus \left\{A\right\}\right)\leftrightarrow \left(\varnothing \in 𝒫A\wedge \varnothing \ne A\right)$$
65	57 63 64	sylanbrc	$$⊢\left(\left(\phi \wedge x\in 𝒫A\right)\wedge x=A\right)\to \varnothing \in \left(𝒫A\setminus \left\{A\right\}\right)$$
66		simplr	$$⊢\left(\left(\phi \wedge x\in 𝒫A\right)\wedge \neg x=A\right)\to x\in 𝒫A$$
67		simpr	$$⊢\left(\left(\phi \wedge x\in 𝒫A\right)\wedge \neg x=A\right)\to \neg x=A$$
68	67	neqned	$$⊢\left(\left(\phi \wedge x\in 𝒫A\right)\wedge \neg x=A\right)\to x\ne A$$
69		eldifsn	$$⊢x\in \left(𝒫A\setminus \left\{A\right\}\right)\leftrightarrow \left(x\in 𝒫A\wedge x\ne A\right)$$
70	66 68 69	sylanbrc	$$⊢\left(\left(\phi \wedge x\in 𝒫A\right)\wedge \neg x=A\right)\to x\in \left(𝒫A\setminus \left\{A\right\}\right)$$
71	65 70	ifclda	$$⊢\left(\phi \wedge x\in 𝒫A\right)\to if\left(x=A,\varnothing ,x\right)\in \left(𝒫A\setminus \left\{A\right\}\right)$$
72	71	fmpttd	$$⊢\phi \to \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right):𝒫A⟶𝒫A\setminus \left\{A\right\}$$
73	55 72	fcod	$$⊢\phi \to \left(\left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\circ \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\right):𝒫A⟶A$$
74	72	frnd	$$⊢\phi \to \mathrm{ran}\left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\subseteq 𝒫A\setminus \left\{A\right\}$$
75		cores	$$⊢\mathrm{ran}\left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\subseteq 𝒫A\setminus \left\{A\right\}\to \left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\circ \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)=\left(G\circ F\right)\circ \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)$$
76	74 75	syl	$$⊢\phi \to \left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\circ \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)=\left(G\circ F\right)\circ \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)$$
77	76 4	eqtr4di	$$⊢\phi \to \left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\circ \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)=H$$
78	77	feq1d	$$⊢\phi \to \left(\left(\left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\circ \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\right):𝒫A⟶A\leftrightarrow H:𝒫A⟶A\right)$$
79	73 78	mpbid	$$⊢\phi \to H:𝒫A⟶A$$
80		inss1	$$⊢𝒫A\cap \mathrm{dom}\mathrm{card}\subseteq 𝒫A$$
81	80	a1i	$$⊢\phi \to 𝒫A\cap \mathrm{dom}\mathrm{card}\subseteq 𝒫A$$
82		eqid	$$⊢{W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]={W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]$$
83	5 6 82	canth4	$$⊢\left(A\in \mathrm{V}\wedge H:𝒫A⟶A\wedge 𝒫A\cap \mathrm{dom}\mathrm{card}\subseteq 𝒫A\right)\to \left(B\subseteq A\wedge {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\subset B\wedge H\left(B\right)=H\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)\right)$$
84	9 79 81 83	syl3anc	$$⊢\phi \to \left(B\subseteq A\wedge {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\subset B\wedge H\left(B\right)=H\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)\right)$$
85	84	simp1d	$$⊢\phi \to B\subseteq A$$
86	84	simp2d	$$⊢\phi \to {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\subset B$$
87	86	pssned	$$⊢\phi \to {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\ne B$$
88	87	necomd	$$⊢\phi \to B\ne {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]$$
89	84	simp3d	$$⊢\phi \to H\left(B\right)=H\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)$$
90	4	fveq1i	$$⊢H\left(B\right)=\left(\left(G\circ F\right)\circ \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\right)\left(B\right)$$
91	4	fveq1i	$$⊢H\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)=\left(\left(G\circ F\right)\circ \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)$$
92	89 90 91	3eqtr3g	$$⊢\phi \to \left(\left(G\circ F\right)\circ \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\right)\left(B\right)=\left(\left(G\circ F\right)\circ \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)$$
93	9 85	sselpwd	$$⊢\phi \to B\in 𝒫A$$
94	72 93	fvco3d	$$⊢\phi \to \left(\left(G\circ F\right)\circ \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\right)\left(B\right)=\left(G\circ F\right)\left(\left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\left(B\right)\right)$$
95	86	pssssd	$$⊢\phi \to {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\subseteq B$$
96	95 85	sstrd	$$⊢\phi \to {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\subseteq A$$
97	9 96	sselpwd	$$⊢\phi \to {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\in 𝒫A$$
98	72 97	fvco3d	$$⊢\phi \to \left(\left(G\circ F\right)\circ \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)=\left(G\circ F\right)\left(\left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)\right)$$
99	92 94 98	3eqtr3d	$$⊢\phi \to \left(G\circ F\right)\left(\left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\left(B\right)\right)=\left(G\circ F\right)\left(\left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)\right)$$
100	99	adantr	$$⊢\left(\phi \wedge B\subset A\right)\to \left(G\circ F\right)\left(\left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\left(B\right)\right)=\left(G\circ F\right)\left(\left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)\right)$$
101		eqid	$$⊢\left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)=\left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)$$
102		eqeq1	$$⊢x=B\to \left(x=A\leftrightarrow B=A\right)$$
103		id	$$⊢x=B\to x=B$$
104	102 103	ifbieq2d	$$⊢x=B\to if\left(x=A,\varnothing ,x\right)=if\left(B=A,\varnothing ,B\right)$$
105		ifcl	$$⊢\left(\varnothing \in 𝒫A\wedge B\in 𝒫A\right)\to if\left(B=A,\varnothing ,B\right)\in 𝒫A$$
106	56 93 105	sylancr	$$⊢\phi \to if\left(B=A,\varnothing ,B\right)\in 𝒫A$$
107	101 104 93 106	fvmptd3	$$⊢\phi \to \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\left(B\right)=if\left(B=A,\varnothing ,B\right)$$
108		pssne	$$⊢B\subset A\to B\ne A$$
109	108	neneqd	$$⊢B\subset A\to \neg B=A$$
110	109	iffalsed	$$⊢B\subset A\to if\left(B=A,\varnothing ,B\right)=B$$
111	107 110	sylan9eq	$$⊢\left(\phi \wedge B\subset A\right)\to \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\left(B\right)=B$$
112	111	fveq2d	$$⊢\left(\phi \wedge B\subset A\right)\to \left(G\circ F\right)\left(\left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\left(B\right)\right)=\left(G\circ F\right)\left(B\right)$$
113		eqeq1	$$⊢x={W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\to \left(x=A\leftrightarrow {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]=A\right)$$
114		id	$$⊢x={W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\to x={W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]$$
115	113 114	ifbieq2d	$$⊢x={W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\to if\left(x=A,\varnothing ,x\right)=if\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]=A,\varnothing ,{W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)$$
116		ifcl	$$⊢\left(\varnothing \in 𝒫A\wedge {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\in 𝒫A\right)\to if\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]=A,\varnothing ,{W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)\in 𝒫A$$
117	56 97 116	sylancr	$$⊢\phi \to if\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]=A,\varnothing ,{W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)\in 𝒫A$$
118	101 115 97 117	fvmptd3	$$⊢\phi \to \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)=if\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]=A,\varnothing ,{W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)$$
119	118	adantr	$$⊢\left(\phi \wedge B\subset A\right)\to \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)=if\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]=A,\varnothing ,{W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)$$
120		sspsstr	$$⊢\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\subseteq B\wedge B\subset A\right)\to {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\subset A$$
121	95 120	sylan	$$⊢\left(\phi \wedge B\subset A\right)\to {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\subset A$$
122	121	pssned	$$⊢\left(\phi \wedge B\subset A\right)\to {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\ne A$$
123	122	neneqd	$$⊢\left(\phi \wedge B\subset A\right)\to \neg {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]=A$$
124	123	iffalsed	$$⊢\left(\phi \wedge B\subset A\right)\to if\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]=A,\varnothing ,{W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)={W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]$$
125	119 124	eqtrd	$$⊢\left(\phi \wedge B\subset A\right)\to \left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)={W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]$$
126	125	fveq2d	$$⊢\left(\phi \wedge B\subset A\right)\to \left(G\circ F\right)\left(\left(x\in 𝒫A⟼if\left(x=A,\varnothing ,x\right)\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)\right)=\left(G\circ F\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)$$
127	100 112 126	3eqtr3d	$$⊢\left(\phi \wedge B\subset A\right)\to \left(G\circ F\right)\left(B\right)=\left(G\circ F\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)$$
128	93 108	anim12i	$$⊢\left(\phi \wedge B\subset A\right)\to \left(B\in 𝒫A\wedge B\ne A\right)$$
129		eldifsn	$$⊢B\in \left(𝒫A\setminus \left\{A\right\}\right)\leftrightarrow \left(B\in 𝒫A\wedge B\ne A\right)$$
130	128 129	sylibr	$$⊢\left(\phi \wedge B\subset A\right)\to B\in \left(𝒫A\setminus \left\{A\right\}\right)$$
131	130	fvresd	$$⊢\left(\phi \wedge B\subset A\right)\to \left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\left(B\right)=\left(G\circ F\right)\left(B\right)$$
132	97	adantr	$$⊢\left(\phi \wedge B\subset A\right)\to {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\in 𝒫A$$
133		eldifsn	$$⊢{W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\in \left(𝒫A\setminus \left\{A\right\}\right)\leftrightarrow \left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\in 𝒫A\wedge {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\ne A\right)$$
134	132 122 133	sylanbrc	$$⊢\left(\phi \wedge B\subset A\right)\to {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\in \left(𝒫A\setminus \left\{A\right\}\right)$$
135	134	fvresd	$$⊢\left(\phi \wedge B\subset A\right)\to \left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)=\left(G\circ F\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)$$
136	127 131 135	3eqtr4d	$$⊢\left(\phi \wedge B\subset A\right)\to \left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\left(B\right)=\left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)$$
137		f1of1	$$⊢\left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right):𝒫A\setminus \left\{A\right\}\underset{1-1\; onto}{⟶}A\to \left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right):𝒫A\setminus \left\{A\right\}\underset{1-1}{⟶}A$$
138	53 137	syl	$$⊢\phi \to \left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right):𝒫A\setminus \left\{A\right\}\underset{1-1}{⟶}A$$
139	138	adantr	$$⊢\left(\phi \wedge B\subset A\right)\to \left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right):𝒫A\setminus \left\{A\right\}\underset{1-1}{⟶}A$$
140		f1fveq	$$⊢\left(\left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right):𝒫A\setminus \left\{A\right\}\underset{1-1}{⟶}A\wedge \left(B\in \left(𝒫A\setminus \left\{A\right\}\right)\wedge {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\in \left(𝒫A\setminus \left\{A\right\}\right)\right)\right)\to \left(\left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\left(B\right)=\left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)\leftrightarrow B={W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)$$
141	139 130 134 140	syl12anc	$$⊢\left(\phi \wedge B\subset A\right)\to \left(\left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\left(B\right)=\left({\left(G\circ F\right)\upharpoonright }_{\left(𝒫A\setminus \left\{A\right\}\right)}\right)\left({W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)\leftrightarrow B={W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)$$
142	136 141	mpbid	$$⊢\left(\phi \wedge B\subset A\right)\to B={W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]$$
143	142	ex	$$⊢\phi \to \left(B\subset A\to B={W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\right)$$
144	143	necon3ad	$$⊢\phi \to \left(B\ne {W\left(B\right)}^{-1}\left[\left\{H\left(B\right)\right\}\right]\to \neg B\subset A\right)$$
145	88 144	mpd	$$⊢\phi \to \neg B\subset A$$
146		npss	$$⊢\neg B\subset A\leftrightarrow \left(B\subseteq A\to B=A\right)$$
147	145 146	sylib	$$⊢\phi \to \left(B\subseteq A\to B=A\right)$$
148	85 147	mpd	$$⊢\phi \to B=A$$
149		eqid	$$⊢B=B$$
150		eqid	$$⊢W\left(B\right)=W\left(B\right)$$
151	149 150	pm3.2i	$$⊢\left(B=B\wedge W\left(B\right)=W\left(B\right)\right)$$
152		elinel1	$$⊢x\in \left(𝒫A\cap \mathrm{dom}\mathrm{card}\right)\to x\in 𝒫A$$
153		ffvelcdm	$$⊢\left(H:𝒫A⟶A\wedge x\in 𝒫A\right)\to H\left(x\right)\in A$$
154	79 152 153	syl2an	$$⊢\left(\phi \wedge x\in \left(𝒫A\cap \mathrm{dom}\mathrm{card}\right)\right)\to H\left(x\right)\in A$$
155	5 9 154 6	fpwwe	$$⊢\phi \to \left(\left(BWW\left(B\right)\wedge H\left(B\right)\in B\right)\leftrightarrow \left(B=B\wedge W\left(B\right)=W\left(B\right)\right)\right)$$
156	151 155	mpbiri	$$⊢\phi \to \left(BWW\left(B\right)\wedge H\left(B\right)\in B\right)$$
157	156	simpld	$$⊢\phi \to BWW\left(B\right)$$
158	5 9	fpwwelem	$$⊢\phi \to \left(BWW\left(B\right)\leftrightarrow \left(\left(B\subseteq A\wedge W\left(B\right)\subseteq B\times B\right)\wedge \left(W\left(B\right)\mathrm{We}B\wedge \forall y\in BH\left({W\left(B\right)}^{-1}\left[\left\{y\right\}\right]\right)=y\right)\right)\right)$$
159	157 158	mpbid	$$⊢\phi \to \left(\left(B\subseteq A\wedge W\left(B\right)\subseteq B\times B\right)\wedge \left(W\left(B\right)\mathrm{We}B\wedge \forall y\in BH\left({W\left(B\right)}^{-1}\left[\left\{y\right\}\right]\right)=y\right)\right)$$
160	159	simprld	$$⊢\phi \to W\left(B\right)\mathrm{We}B$$
161		fvex	$$⊢W\left(B\right)\in \mathrm{V}$$
162		weeq1	$$⊢r=W\left(B\right)\to \left(r\mathrm{We}B\leftrightarrow W\left(B\right)\mathrm{We}B\right)$$
163	161 162	spcev	$$⊢W\left(B\right)\mathrm{We}B\to \exists rr\mathrm{We}B$$
164	160 163	syl	$$⊢\phi \to \exists rr\mathrm{We}B$$
165		ween	$$⊢B\in \mathrm{dom}\mathrm{card}\leftrightarrow \exists rr\mathrm{We}B$$
166	164 165	sylibr	$$⊢\phi \to B\in \mathrm{dom}\mathrm{card}$$
167	148 166	eqeltrrd	$$⊢\phi \to A\in \mathrm{dom}\mathrm{card}$$
168		domtri2	$$⊢\left(\mathrm{\omega }\in \mathrm{dom}\mathrm{card}\wedge A\in \mathrm{dom}\mathrm{card}\right)\to \left(\mathrm{\omega }\preccurlyeq A\leftrightarrow \neg A\prec \mathrm{\omega }\right)$$
169	23 167 168	sylancr	$$⊢\phi \to \left(\mathrm{\omega }\preccurlyeq A\leftrightarrow \neg A\prec \mathrm{\omega }\right)$$
170		infdju1	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx A$$
171	169 170	syl6bir	$$⊢\phi \to \left(\neg A\prec \mathrm{\omega }\to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx A\right)$$
172		ensym	$$⊢\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx A\to A\approx \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)$$
173	171 172	syl6	$$⊢\phi \to \left(\neg A\prec \mathrm{\omega }\to A\approx \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\right)$$
174	20 173	mt3d	$$⊢\phi \to A\prec \mathrm{\omega }$$
175		2onn	$$⊢2_{𝑜}\in \mathrm{\omega }$$
176		nnsdom	$$⊢2_{𝑜}\in \mathrm{\omega }\to 2_{𝑜}\prec \mathrm{\omega }$$
177	175 176	ax-mp	$$⊢2_{𝑜}\prec \mathrm{\omega }$$
178		djufi	$$⊢\left(A\prec \mathrm{\omega }\wedge 2_{𝑜}\prec \mathrm{\omega }\right)\to \left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)\prec \mathrm{\omega }$$
179	174 177 178	sylancl	$$⊢\phi \to \left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)\prec \mathrm{\omega }$$
180		isfinite	$$⊢\left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)\in \mathrm{Fin}\leftrightarrow \left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)\prec \mathrm{\omega }$$
181	179 180	sylibr	$$⊢\phi \to \left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)\in \mathrm{Fin}$$
182		sssucid	$$⊢1_{𝑜}\subseteq \mathrm{suc}{1}_{𝑜}$$
183		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
184	182 183	sseqtrri	$$⊢1_{𝑜}\subseteq 2_{𝑜}$$
185		xpss2	$$⊢1_{𝑜}\subseteq 2_{𝑜}\to \left\{1_{𝑜}\right\}\times 1_{𝑜}\subseteq \left\{1_{𝑜}\right\}\times 2_{𝑜}$$
186	184 185	ax-mp	$$⊢\left\{1_{𝑜}\right\}\times 1_{𝑜}\subseteq \left\{1_{𝑜}\right\}\times 2_{𝑜}$$
187		unss2	$$⊢\left\{1_{𝑜}\right\}\times 1_{𝑜}\subseteq \left\{1_{𝑜}\right\}\times 2_{𝑜}\to \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\subseteq \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 2_{𝑜}\right)$$
188	186 187	mp1i	$$⊢\phi \to \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\subseteq \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 2_{𝑜}\right)$$
189		ssun2	$$⊢\left\{1_{𝑜}\right\}\times 2_{𝑜}\subseteq \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 2_{𝑜}\right)$$
190		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
191	190	snid	$$⊢1_{𝑜}\in \left\{1_{𝑜}\right\}$$
192	190	sucid	$$⊢1_{𝑜}\in \mathrm{suc}{1}_{𝑜}$$
193	192 183	eleqtrri	$$⊢1_{𝑜}\in 2_{𝑜}$$
194		opelxpi	$$⊢\left(1_{𝑜}\in \left\{1_{𝑜}\right\}\wedge 1_{𝑜}\in 2_{𝑜}\right)\to ⟨1_{𝑜},1_{𝑜}⟩\in \left(\left\{1_{𝑜}\right\}\times 2_{𝑜}\right)$$
195	191 193 194	mp2an	$$⊢⟨1_{𝑜},1_{𝑜}⟩\in \left(\left\{1_{𝑜}\right\}\times 2_{𝑜}\right)$$
196	189 195	sselii	$$⊢⟨1_{𝑜},1_{𝑜}⟩\in \left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 2_{𝑜}\right)\right)$$
197		1n0	$$⊢1_{𝑜}\ne \varnothing$$
198	197	neii	$$⊢\neg 1_{𝑜}=\varnothing$$
199		opelxp1	$$⊢⟨1_{𝑜},1_{𝑜}⟩\in \left(\left\{\varnothing \right\}\times A\right)\to 1_{𝑜}\in \left\{\varnothing \right\}$$
200		elsni	$$⊢1_{𝑜}\in \left\{\varnothing \right\}\to 1_{𝑜}=\varnothing$$
201	199 200	syl	$$⊢⟨1_{𝑜},1_{𝑜}⟩\in \left(\left\{\varnothing \right\}\times A\right)\to 1_{𝑜}=\varnothing$$
202	198 201	mto	$$⊢\neg ⟨1_{𝑜},1_{𝑜}⟩\in \left(\left\{\varnothing \right\}\times A\right)$$
203		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
204		nnord	$$⊢1_{𝑜}\in \mathrm{\omega }\to \mathrm{Ord}{1}_{𝑜}$$
205		ordirr	$$⊢\mathrm{Ord}{1}_{𝑜}\to \neg 1_{𝑜}\in 1_{𝑜}$$
206	203 204 205	mp2b	$$⊢\neg 1_{𝑜}\in 1_{𝑜}$$
207		opelxp2	$$⊢⟨1_{𝑜},1_{𝑜}⟩\in \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\to 1_{𝑜}\in 1_{𝑜}$$
208	206 207	mto	$$⊢\neg ⟨1_{𝑜},1_{𝑜}⟩\in \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)$$
209	202 208	pm3.2ni	$$⊢\neg \left(⟨1_{𝑜},1_{𝑜}⟩\in \left(\left\{\varnothing \right\}\times A\right)\vee ⟨1_{𝑜},1_{𝑜}⟩\in \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\right)$$
210		elun	$$⊢⟨1_{𝑜},1_{𝑜}⟩\in \left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\right)\leftrightarrow \left(⟨1_{𝑜},1_{𝑜}⟩\in \left(\left\{\varnothing \right\}\times A\right)\vee ⟨1_{𝑜},1_{𝑜}⟩\in \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\right)$$
211	209 210	mtbir	$$⊢\neg ⟨1_{𝑜},1_{𝑜}⟩\in \left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\right)$$
212		ssnelpss	$$⊢\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\subseteq \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 2_{𝑜}\right)\to \left(\left(⟨1_{𝑜},1_{𝑜}⟩\in \left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 2_{𝑜}\right)\right)\wedge \neg ⟨1_{𝑜},1_{𝑜}⟩\in \left(\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\right)\right)\to \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\subset \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 2_{𝑜}\right)\right)$$
213	196 211 212	mp2ani	$$⊢\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\subseteq \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 2_{𝑜}\right)\to \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\subset \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 2_{𝑜}\right)$$
214	188 213	syl	$$⊢\phi \to \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\subset \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 2_{𝑜}\right)$$
215		df-dju	$$⊢\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)=\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)$$
216		df-dju	$$⊢\left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)=\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 2_{𝑜}\right)$$
217	215 216	psseq12i	$$⊢\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\subset \left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)\leftrightarrow \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 1_{𝑜}\right)\subset \left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times 2_{𝑜}\right)$$
218	214 217	sylibr	$$⊢\phi \to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\subset \left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)$$
219		php3	$$⊢\left(\left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)\in \mathrm{Fin}\wedge \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\subset \left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)\right)\to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\prec \left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)$$
220	181 218 219	syl2anc	$$⊢\phi \to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\prec \left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)$$
221		canthp1lem1	$$⊢1_{𝑜}\prec A\to \left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)\preccurlyeq 𝒫A$$
222	1 221	syl	$$⊢\phi \to \left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)\preccurlyeq 𝒫A$$
223		sdomdomtr	$$⊢\left(\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\prec \left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)\wedge \left(A\mathrm{\bigsqcup ︀}{2}_{𝑜}\right)\preccurlyeq 𝒫A\right)\to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\prec 𝒫A$$
224	220 222 223	syl2anc	$$⊢\phi \to \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\prec 𝒫A$$
225		sdomnen	$$⊢\left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\prec 𝒫A\to \neg \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx 𝒫A$$
226	224 225	syl	$$⊢\phi \to \neg \left(A\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx 𝒫A$$
227	13 226	pm2.65i	$$⊢\neg \phi$$