Theorem unxpwdom2

Description: Lemma for unxpwdom . (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	unxpwdom2	$$⊢\left(A\times A\right)\approx \left(B\cup C\right)\to \left(A{\preccurlyeq }^{*}B\vee A\preccurlyeq C\right)$$

Proof

Step	Hyp	Ref	Expression
1		ensym	$$⊢\left(A\times A\right)\approx \left(B\cup C\right)\to \left(B\cup C\right)\approx \left(A\times A\right)$$
2		bren	$$⊢\left(B\cup C\right)\approx \left(A\times A\right)\leftrightarrow \exists ff:B\cup C\underset{1-1\; onto}{⟶}A\times A$$
3		ssdif0	$$⊢A\subseteq \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\leftrightarrow A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]=\varnothing$$
4		dmxpid	$$⊢\mathrm{dom}\left(A\times A\right)=A$$
5		f1ofo	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to f:B\cup C\underset{onto}{⟶}A\times A$$
6		forn	$$⊢f:B\cup C\underset{onto}{⟶}A\times A\to \mathrm{ran}f=A\times A$$
7	5 6	syl	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \mathrm{ran}f=A\times A$$
8		vex	$$⊢f\in \mathrm{V}$$
9	8	rnex	$$⊢\mathrm{ran}f\in \mathrm{V}$$
10	7 9	eqeltrrdi	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to A\times A\in \mathrm{V}$$
11	10	dmexd	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \mathrm{dom}\left(A\times A\right)\in \mathrm{V}$$
12	4 11	eqeltrrid	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to A\in \mathrm{V}$$
13		imassrn	$$⊢\left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\subseteq \mathrm{ran}\left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)$$
14		f1stres	$$⊢\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right):A\times A⟶A$$
15		f1of	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to f:B\cup C⟶A\times A$$
16		fco	$$⊢\left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right):A\times A⟶A\wedge f:B\cup C⟶A\times A\right)\to \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right):B\cup C⟶A$$
17	14 15 16	sylancr	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right):B\cup C⟶A$$
18	17	frnd	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \mathrm{ran}\left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\subseteq A$$
19	13 18	sstrid	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\subseteq A$$
20	12 19	ssexd	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\in \mathrm{V}$$
21	20	adantr	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge A\subseteq \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\to \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\in \mathrm{V}$$
22		simpr	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge A\subseteq \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\to A\subseteq \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]$$
23		ssdomg	$$⊢\left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\in \mathrm{V}\to \left(A\subseteq \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\to A\preccurlyeq \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)$$
24	21 22 23	sylc	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge A\subseteq \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\to A\preccurlyeq \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]$$
25		domwdom	$$⊢A\preccurlyeq \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\to A{\preccurlyeq }^{*}\left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]$$
26	24 25	syl	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge A\subseteq \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\to A{\preccurlyeq }^{*}\left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]$$
27	17	ffund	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \mathrm{Fun}\left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)$$
28		ssun1	$$⊢B\subseteq B\cup C$$
29		f1odm	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \mathrm{dom}f=B\cup C$$
30	8	dmex	$$⊢\mathrm{dom}f\in \mathrm{V}$$
31	29 30	eqeltrrdi	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to B\cup C\in \mathrm{V}$$
32		ssexg	$$⊢\left(B\subseteq B\cup C\wedge B\cup C\in \mathrm{V}\right)\to B\in \mathrm{V}$$
33	28 31 32	sylancr	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to B\in \mathrm{V}$$
34		wdomima2g	$$⊢\left(\mathrm{Fun}\left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\wedge B\in \mathrm{V}\wedge \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\in \mathrm{V}\right)\to \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]{\preccurlyeq }^{*}B$$
35	27 33 20 34	syl3anc	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]{\preccurlyeq }^{*}B$$
36	35	adantr	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge A\subseteq \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\to \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]{\preccurlyeq }^{*}B$$
37		wdomtr	$$⊢\left(A{\preccurlyeq }^{*}\left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\wedge \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]{\preccurlyeq }^{*}B\right)\to A{\preccurlyeq }^{*}B$$
38	26 36 37	syl2anc	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge A\subseteq \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\to A{\preccurlyeq }^{*}B$$
39	38	orcd	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge A\subseteq \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\to \left(A{\preccurlyeq }^{*}B\vee A\preccurlyeq C\right)$$
40	39	ex	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \left(A\subseteq \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\to \left(A{\preccurlyeq }^{*}B\vee A\preccurlyeq C\right)\right)$$
41	3 40	syl5bir	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]=\varnothing \to \left(A{\preccurlyeq }^{*}B\vee A\preccurlyeq C\right)\right)$$
42		n0	$$⊢A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\ne \varnothing \leftrightarrow \exists xx\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)$$
43		ssun2	$$⊢C\subseteq B\cup C$$
44		ssexg	$$⊢\left(C\subseteq B\cup C\wedge B\cup C\in \mathrm{V}\right)\to C\in \mathrm{V}$$
45	43 31 44	sylancr	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to C\in \mathrm{V}$$
46	45	adantr	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to C\in \mathrm{V}$$
47		f1ofn	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to fFn\left(B\cup C\right)$$
48		elpreima	$$⊢fFn\left(B\cup C\right)\to \left(y\in f^{-1}\left[\left\{x\right\}\times A\right]\leftrightarrow \left(y\in \left(B\cup C\right)\wedge f\left(y\right)\in \left(\left\{x\right\}\times A\right)\right)\right)$$
49	47 48	syl	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \left(y\in f^{-1}\left[\left\{x\right\}\times A\right]\leftrightarrow \left(y\in \left(B\cup C\right)\wedge f\left(y\right)\in \left(\left\{x\right\}\times A\right)\right)\right)$$
50	49	adantr	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to \left(y\in f^{-1}\left[\left\{x\right\}\times A\right]\leftrightarrow \left(y\in \left(B\cup C\right)\wedge f\left(y\right)\in \left(\left\{x\right\}\times A\right)\right)\right)$$
51		elun	$$⊢y\in \left(B\cup C\right)\leftrightarrow \left(y\in B\vee y\in C\right)$$
52		df-or	$$⊢\left(y\in B\vee y\in C\right)\leftrightarrow \left(\neg y\in B\to y\in C\right)$$
53	51 52	bitri	$$⊢y\in \left(B\cup C\right)\leftrightarrow \left(\neg y\in B\to y\in C\right)$$
54		eldifn	$$⊢x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\to \neg x\in \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]$$
55	54	ad2antlr	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge f\left(y\right)\in \left(\left\{x\right\}\times A\right)\right)\to \neg x\in \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]$$
56	15	ad2antrr	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to f:B\cup C⟶A\times A$$
57		simprr	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to y\in B$$
58	28 57	sselid	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to y\in \left(B\cup C\right)$$
59		fvco3	$$⊢\left(f:B\cup C⟶A\times A\wedge y\in \left(B\cup C\right)\right)\to \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left(y\right)=\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\left(f\left(y\right)\right)$$
60	56 58 59	syl2anc	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left(y\right)=\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\left(f\left(y\right)\right)$$
61		eldifi	$$⊢x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\to x\in A$$
62	61	adantl	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to x\in A$$
63	62	snssd	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to \left\{x\right\}\subseteq A$$
64		xpss1	$$⊢\left\{x\right\}\subseteq A\to \left\{x\right\}\times A\subseteq A\times A$$
65	63 64	syl	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to \left\{x\right\}\times A\subseteq A\times A$$
66	65	adantr	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to \left\{x\right\}\times A\subseteq A\times A$$
67		simprl	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to f\left(y\right)\in \left(\left\{x\right\}\times A\right)$$
68	66 67	sseldd	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to f\left(y\right)\in \left(A\times A\right)$$
69	68	fvresd	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to \left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\left(f\left(y\right)\right)=1^{st}\left(f\left(y\right)\right)$$
70		xp1st	$$⊢f\left(y\right)\in \left(\left\{x\right\}\times A\right)\to 1^{st}\left(f\left(y\right)\right)\in \left\{x\right\}$$
71	67 70	syl	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to 1^{st}\left(f\left(y\right)\right)\in \left\{x\right\}$$
72	69 71	eqeltrd	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to \left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\left(f\left(y\right)\right)\in \left\{x\right\}$$
73		elsni	$$⊢\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\left(f\left(y\right)\right)\in \left\{x\right\}\to \left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\left(f\left(y\right)\right)=x$$
74	72 73	syl	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to \left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\left(f\left(y\right)\right)=x$$
75	60 74	eqtrd	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left(y\right)=x$$
76	17	ffnd	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)Fn\left(B\cup C\right)$$
77	76	ad2antrr	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)Fn\left(B\cup C\right)$$
78	28	a1i	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to B\subseteq B\cup C$$
79		fnfvima	$$⊢\left(\left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)Fn\left(B\cup C\right)\wedge B\subseteq B\cup C\wedge y\in B\right)\to \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left(y\right)\in \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]$$
80	77 78 57 79	syl3anc	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left(y\right)\in \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]$$
81	75 80	eqeltrrd	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\wedge y\in B\right)\right)\to x\in \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]$$
82	81	expr	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge f\left(y\right)\in \left(\left\{x\right\}\times A\right)\right)\to \left(y\in B\to x\in \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)$$
83	55 82	mtod	$$⊢\left(\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\wedge f\left(y\right)\in \left(\left\{x\right\}\times A\right)\right)\to \neg y\in B$$
84	83	ex	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\to \neg y\in B\right)$$
85	84	imim1d	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to \left(\left(\neg y\in B\to y\in C\right)\to \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\to y\in C\right)\right)$$
86	53 85	syl5bi	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to \left(y\in \left(B\cup C\right)\to \left(f\left(y\right)\in \left(\left\{x\right\}\times A\right)\to y\in C\right)\right)$$
87	86	impd	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to \left(\left(y\in \left(B\cup C\right)\wedge f\left(y\right)\in \left(\left\{x\right\}\times A\right)\right)\to y\in C\right)$$
88	50 87	sylbid	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to \left(y\in f^{-1}\left[\left\{x\right\}\times A\right]\to y\in C\right)$$
89	88	ssrdv	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to f^{-1}\left[\left\{x\right\}\times A\right]\subseteq C$$
90		ssdomg	$$⊢C\in \mathrm{V}\to \left(f^{-1}\left[\left\{x\right\}\times A\right]\subseteq C\to f^{-1}\left[\left\{x\right\}\times A\right]\preccurlyeq C\right)$$
91	46 89 90	sylc	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to f^{-1}\left[\left\{x\right\}\times A\right]\preccurlyeq C$$
92		f1ocnv	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to f^{-1}:A\times A\underset{1-1\; onto}{⟶}B\cup C$$
93		f1of1	$$⊢f^{-1}:A\times A\underset{1-1\; onto}{⟶}B\cup C\to f^{-1}:A\times A\underset{1-1}{⟶}B\cup C$$
94	92 93	syl	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to f^{-1}:A\times A\underset{1-1}{⟶}B\cup C$$
95	94	adantr	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to f^{-1}:A\times A\underset{1-1}{⟶}B\cup C$$
96	31	adantr	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to B\cup C\in \mathrm{V}$$
97		snex	$$⊢\left\{x\right\}\in \mathrm{V}$$
98	12	adantr	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to A\in \mathrm{V}$$
99		xpexg	$$⊢\left(\left\{x\right\}\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \left\{x\right\}\times A\in \mathrm{V}$$
100	97 98 99	sylancr	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to \left\{x\right\}\times A\in \mathrm{V}$$
101		f1imaen2g	$$⊢\left(\left(f^{-1}:A\times A\underset{1-1}{⟶}B\cup C\wedge B\cup C\in \mathrm{V}\right)\wedge \left(\left\{x\right\}\times A\subseteq A\times A\wedge \left\{x\right\}\times A\in \mathrm{V}\right)\right)\to f^{-1}\left[\left\{x\right\}\times A\right]\approx \left(\left\{x\right\}\times A\right)$$
102	95 96 65 100 101	syl22anc	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to f^{-1}\left[\left\{x\right\}\times A\right]\approx \left(\left\{x\right\}\times A\right)$$
103		vex	$$⊢x\in \mathrm{V}$$
104		xpsnen2g	$$⊢\left(x\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \left(\left\{x\right\}\times A\right)\approx A$$
105	103 98 104	sylancr	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to \left(\left\{x\right\}\times A\right)\approx A$$
106		entr	$$⊢\left(f^{-1}\left[\left\{x\right\}\times A\right]\approx \left(\left\{x\right\}\times A\right)\wedge \left(\left\{x\right\}\times A\right)\approx A\right)\to f^{-1}\left[\left\{x\right\}\times A\right]\approx A$$
107	102 105 106	syl2anc	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to f^{-1}\left[\left\{x\right\}\times A\right]\approx A$$
108		domen1	$$⊢f^{-1}\left[\left\{x\right\}\times A\right]\approx A\to \left(f^{-1}\left[\left\{x\right\}\times A\right]\preccurlyeq C\leftrightarrow A\preccurlyeq C\right)$$
109	107 108	syl	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to \left(f^{-1}\left[\left\{x\right\}\times A\right]\preccurlyeq C\leftrightarrow A\preccurlyeq C\right)$$
110	91 109	mpbid	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to A\preccurlyeq C$$
111	110	olcd	$$⊢\left(f:B\cup C\underset{1-1\; onto}{⟶}A\times A\wedge x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\right)\to \left(A{\preccurlyeq }^{*}B\vee A\preccurlyeq C\right)$$
112	111	ex	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \left(x\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\to \left(A{\preccurlyeq }^{*}B\vee A\preccurlyeq C\right)\right)$$
113	112	exlimdv	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \left(\exists xx\in \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\right)\to \left(A{\preccurlyeq }^{*}B\vee A\preccurlyeq C\right)\right)$$
114	42 113	syl5bi	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \left(A\setminus \left(\left({1^{st}\upharpoonright }_{\left(A\times A\right)}\right)\circ f\right)\left[B\right]\ne \varnothing \to \left(A{\preccurlyeq }^{*}B\vee A\preccurlyeq C\right)\right)$$
115	41 114	pm2.61dne	$$⊢f:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \left(A{\preccurlyeq }^{*}B\vee A\preccurlyeq C\right)$$
116	115	exlimiv	$$⊢\exists ff:B\cup C\underset{1-1\; onto}{⟶}A\times A\to \left(A{\preccurlyeq }^{*}B\vee A\preccurlyeq C\right)$$
117	2 116	sylbi	$$⊢\left(B\cup C\right)\approx \left(A\times A\right)\to \left(A{\preccurlyeq }^{*}B\vee A\preccurlyeq C\right)$$
118	1 117	syl	$$⊢\left(A\times A\right)\approx \left(B\cup C\right)\to \left(A{\preccurlyeq }^{*}B\vee A\preccurlyeq C\right)$$