Theorem domunsncan

Description: A singleton cancellation law for dominance. (Contributed by Stefan O'Rear, 19-Feb-2015) (Revised by Stefan O'Rear, 5-May-2015)

	Ref	Expression
Hypotheses	domunsncan.a	$$⊢A\in \mathrm{V}$$
	domunsncan.b	$$⊢B\in \mathrm{V}$$
Assertion	domunsncan	$$⊢\left(\neg A\in X\wedge \neg B\in Y\right)\to \left(\left(\left\{A\right\}\cup X\right)\preccurlyeq \left(\left\{B\right\}\cup Y\right)\leftrightarrow X\preccurlyeq Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		domunsncan.a	$$⊢A\in \mathrm{V}$$
2		domunsncan.b	$$⊢B\in \mathrm{V}$$
3		ssun2	$$⊢Y\subseteq \left\{B\right\}\cup Y$$
4		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
5	4	brrelex2i	$$⊢\left(\left\{A\right\}\cup X\right)\preccurlyeq \left(\left\{B\right\}\cup Y\right)\to \left\{B\right\}\cup Y\in \mathrm{V}$$
6	5	adantl	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(\left\{A\right\}\cup X\right)\preccurlyeq \left(\left\{B\right\}\cup Y\right)\right)\to \left\{B\right\}\cup Y\in \mathrm{V}$$
7		ssexg	$$⊢\left(Y\subseteq \left\{B\right\}\cup Y\wedge \left\{B\right\}\cup Y\in \mathrm{V}\right)\to Y\in \mathrm{V}$$
8	3 6 7	sylancr	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(\left\{A\right\}\cup X\right)\preccurlyeq \left(\left\{B\right\}\cup Y\right)\right)\to Y\in \mathrm{V}$$
9		brdomi	$$⊢\left(\left\{A\right\}\cup X\right)\preccurlyeq \left(\left\{B\right\}\cup Y\right)\to \exists ff:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y$$
10		vex	$$⊢f\in \mathrm{V}$$
11	10	resex	$$⊢{f\upharpoonright }_{\left(\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right)}\in \mathrm{V}$$
12		simprr	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y$$
13		difss	$$⊢\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\subseteq \left\{A\right\}\cup X$$
14		f1ores	$$⊢\left(f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\wedge \left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\subseteq \left\{A\right\}\cup X\right)\to \left({f\upharpoonright }_{\left(\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right)}\right):\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\underset{1-1\; onto}{⟶}f\left[\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right]$$
15	12 13 14	sylancl	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to \left({f\upharpoonright }_{\left(\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right)}\right):\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\underset{1-1\; onto}{⟶}f\left[\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right]$$
16		f1oen3g	$$⊢\left({f\upharpoonright }_{\left(\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right)}\in \mathrm{V}\wedge \left({f\upharpoonright }_{\left(\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right)}\right):\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\underset{1-1\; onto}{⟶}f\left[\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right]\right)\to \left(\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right)\approx f\left[\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right]$$
17	11 15 16	sylancr	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to \left(\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right)\approx f\left[\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right]$$
18		df-f1	$$⊢f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\leftrightarrow \left(f:\left\{A\right\}\cup X⟶\left\{B\right\}\cup Y\wedge \mathrm{Fun}{f}^{-1}\right)$$
19		imadif	$$⊢\mathrm{Fun}{f}^{-1}\to f\left[\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right]=f\left[\left\{A\right\}\cup X\right]\setminus f\left[\left\{A\right\}\right]$$
20	18 19	simplbiim	$$⊢f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\to f\left[\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right]=f\left[\left\{A\right\}\cup X\right]\setminus f\left[\left\{A\right\}\right]$$
21	20	ad2antll	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to f\left[\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right]=f\left[\left\{A\right\}\cup X\right]\setminus f\left[\left\{A\right\}\right]$$
22		snex	$$⊢\left\{B\right\}\in \mathrm{V}$$
23		simprl	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to Y\in \mathrm{V}$$
24		unexg	$$⊢\left(\left\{B\right\}\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\to \left\{B\right\}\cup Y\in \mathrm{V}$$
25	22 23 24	sylancr	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to \left\{B\right\}\cup Y\in \mathrm{V}$$
26	25	difexd	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to \left(\left\{B\right\}\cup Y\right)\setminus \left\{f\left(A\right)\right\}\in \mathrm{V}$$
27		f1f	$$⊢f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\to f:\left\{A\right\}\cup X⟶\left\{B\right\}\cup Y$$
28		fimass	$$⊢f:\left\{A\right\}\cup X⟶\left\{B\right\}\cup Y\to f\left[\left\{A\right\}\cup X\right]\subseteq \left\{B\right\}\cup Y$$
29	27 28	syl	$$⊢f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\to f\left[\left\{A\right\}\cup X\right]\subseteq \left\{B\right\}\cup Y$$
30	29	ad2antll	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to f\left[\left\{A\right\}\cup X\right]\subseteq \left\{B\right\}\cup Y$$
31	30	ssdifd	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to f\left[\left\{A\right\}\cup X\right]\setminus f\left[\left\{A\right\}\right]\subseteq \left(\left\{B\right\}\cup Y\right)\setminus f\left[\left\{A\right\}\right]$$
32		f1fn	$$⊢f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\to fFn\left(\left\{A\right\}\cup X\right)$$
33	32	ad2antll	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to fFn\left(\left\{A\right\}\cup X\right)$$
34	1	snid	$$⊢A\in \left\{A\right\}$$
35		elun1	$$⊢A\in \left\{A\right\}\to A\in \left(\left\{A\right\}\cup X\right)$$
36	34 35	ax-mp	$$⊢A\in \left(\left\{A\right\}\cup X\right)$$
37		fnsnfv	$$⊢\left(fFn\left(\left\{A\right\}\cup X\right)\wedge A\in \left(\left\{A\right\}\cup X\right)\right)\to \left\{f\left(A\right)\right\}=f\left[\left\{A\right\}\right]$$
38	33 36 37	sylancl	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to \left\{f\left(A\right)\right\}=f\left[\left\{A\right\}\right]$$
39	38	difeq2d	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to \left(\left\{B\right\}\cup Y\right)\setminus \left\{f\left(A\right)\right\}=\left(\left\{B\right\}\cup Y\right)\setminus f\left[\left\{A\right\}\right]$$
40	31 39	sseqtrrd	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to f\left[\left\{A\right\}\cup X\right]\setminus f\left[\left\{A\right\}\right]\subseteq \left(\left\{B\right\}\cup Y\right)\setminus \left\{f\left(A\right)\right\}$$
41		ssdomg	$$⊢\left(\left\{B\right\}\cup Y\right)\setminus \left\{f\left(A\right)\right\}\in \mathrm{V}\to \left(f\left[\left\{A\right\}\cup X\right]\setminus f\left[\left\{A\right\}\right]\subseteq \left(\left\{B\right\}\cup Y\right)\setminus \left\{f\left(A\right)\right\}\to \left(f\left[\left\{A\right\}\cup X\right]\setminus f\left[\left\{A\right\}\right]\right)\preccurlyeq \left(\left(\left\{B\right\}\cup Y\right)\setminus \left\{f\left(A\right)\right\}\right)\right)$$
42	26 40 41	sylc	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to \left(f\left[\left\{A\right\}\cup X\right]\setminus f\left[\left\{A\right\}\right]\right)\preccurlyeq \left(\left(\left\{B\right\}\cup Y\right)\setminus \left\{f\left(A\right)\right\}\right)$$
43		ffvelcdm	$$⊢\left(f:\left\{A\right\}\cup X⟶\left\{B\right\}\cup Y\wedge A\in \left(\left\{A\right\}\cup X\right)\right)\to f\left(A\right)\in \left(\left\{B\right\}\cup Y\right)$$
44	27 36 43	sylancl	$$⊢f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\to f\left(A\right)\in \left(\left\{B\right\}\cup Y\right)$$
45	44	ad2antll	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to f\left(A\right)\in \left(\left\{B\right\}\cup Y\right)$$
46	2	snid	$$⊢B\in \left\{B\right\}$$
47		elun1	$$⊢B\in \left\{B\right\}\to B\in \left(\left\{B\right\}\cup Y\right)$$
48	46 47	mp1i	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to B\in \left(\left\{B\right\}\cup Y\right)$$
49		difsnen	$$⊢\left(\left\{B\right\}\cup Y\in \mathrm{V}\wedge f\left(A\right)\in \left(\left\{B\right\}\cup Y\right)\wedge B\in \left(\left\{B\right\}\cup Y\right)\right)\to \left(\left(\left\{B\right\}\cup Y\right)\setminus \left\{f\left(A\right)\right\}\right)\approx \left(\left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}\right)$$
50	25 45 48 49	syl3anc	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to \left(\left(\left\{B\right\}\cup Y\right)\setminus \left\{f\left(A\right)\right\}\right)\approx \left(\left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}\right)$$
51		domentr	$$⊢\left(\left(f\left[\left\{A\right\}\cup X\right]\setminus f\left[\left\{A\right\}\right]\right)\preccurlyeq \left(\left(\left\{B\right\}\cup Y\right)\setminus \left\{f\left(A\right)\right\}\right)\wedge \left(\left(\left\{B\right\}\cup Y\right)\setminus \left\{f\left(A\right)\right\}\right)\approx \left(\left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}\right)\right)\to \left(f\left[\left\{A\right\}\cup X\right]\setminus f\left[\left\{A\right\}\right]\right)\preccurlyeq \left(\left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}\right)$$
52	42 50 51	syl2anc	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to \left(f\left[\left\{A\right\}\cup X\right]\setminus f\left[\left\{A\right\}\right]\right)\preccurlyeq \left(\left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}\right)$$
53	21 52	eqbrtrd	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to f\left[\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right]\preccurlyeq \left(\left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}\right)$$
54		endomtr	$$⊢\left(\left(\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right)\approx f\left[\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right]\wedge f\left[\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right]\preccurlyeq \left(\left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}\right)\right)\to \left(\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right)\preccurlyeq \left(\left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}\right)$$
55	17 53 54	syl2anc	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to \left(\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}\right)\preccurlyeq \left(\left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}\right)$$
56		uncom	$$⊢\left\{A\right\}\cup X=X\cup \left\{A\right\}$$
57	56	difeq1i	$$⊢\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}=\left(X\cup \left\{A\right\}\right)\setminus \left\{A\right\}$$
58		difun2	$$⊢\left(X\cup \left\{A\right\}\right)\setminus \left\{A\right\}=X\setminus \left\{A\right\}$$
59	57 58	eqtri	$$⊢\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}=X\setminus \left\{A\right\}$$
60		difsn	$$⊢\neg A\in X\to X\setminus \left\{A\right\}=X$$
61	59 60	eqtrid	$$⊢\neg A\in X\to \left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}=X$$
62	61	ad2antrr	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to \left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}=X$$
63		uncom	$$⊢\left\{B\right\}\cup Y=Y\cup \left\{B\right\}$$
64	63	difeq1i	$$⊢\left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}=\left(Y\cup \left\{B\right\}\right)\setminus \left\{B\right\}$$
65		difun2	$$⊢\left(Y\cup \left\{B\right\}\right)\setminus \left\{B\right\}=Y\setminus \left\{B\right\}$$
66	64 65	eqtri	$$⊢\left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}=Y\setminus \left\{B\right\}$$
67		difsn	$$⊢\neg B\in Y\to Y\setminus \left\{B\right\}=Y$$
68	66 67	eqtrid	$$⊢\neg B\in Y\to \left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}=Y$$
69	68	ad2antlr	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to \left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}=Y$$
70	55 62 69	3brtr3d	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(Y\in \mathrm{V}\wedge f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\right)\right)\to X\preccurlyeq Y$$
71	70	expr	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge Y\in \mathrm{V}\right)\to \left(f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\to X\preccurlyeq Y\right)$$
72	71	exlimdv	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge Y\in \mathrm{V}\right)\to \left(\exists ff:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\to X\preccurlyeq Y\right)$$
73	9 72	syl5	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge Y\in \mathrm{V}\right)\to \left(\left(\left\{A\right\}\cup X\right)\preccurlyeq \left(\left\{B\right\}\cup Y\right)\to X\preccurlyeq Y\right)$$
74	73	impancom	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(\left\{A\right\}\cup X\right)\preccurlyeq \left(\left\{B\right\}\cup Y\right)\right)\to \left(Y\in \mathrm{V}\to X\preccurlyeq Y\right)$$
75	8 74	mpd	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge \left(\left\{A\right\}\cup X\right)\preccurlyeq \left(\left\{B\right\}\cup Y\right)\right)\to X\preccurlyeq Y$$
76		en2sn	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left\{A\right\}\approx \left\{B\right\}$$
77	1 2 76	mp2an	$$⊢\left\{A\right\}\approx \left\{B\right\}$$
78		endom	$$⊢\left\{A\right\}\approx \left\{B\right\}\to \left\{A\right\}\preccurlyeq \left\{B\right\}$$
79	77 78	mp1i	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge X\preccurlyeq Y\right)\to \left\{A\right\}\preccurlyeq \left\{B\right\}$$
80		simpr	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge X\preccurlyeq Y\right)\to X\preccurlyeq Y$$
81		incom	$$⊢\left\{B\right\}\cap Y=Y\cap \left\{B\right\}$$
82		disjsn	$$⊢Y\cap \left\{B\right\}=\varnothing \leftrightarrow \neg B\in Y$$
83	82	biimpri	$$⊢\neg B\in Y\to Y\cap \left\{B\right\}=\varnothing$$
84	81 83	eqtrid	$$⊢\neg B\in Y\to \left\{B\right\}\cap Y=\varnothing$$
85	84	ad2antlr	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge X\preccurlyeq Y\right)\to \left\{B\right\}\cap Y=\varnothing$$
86		undom	$$⊢\left(\left(\left\{A\right\}\preccurlyeq \left\{B\right\}\wedge X\preccurlyeq Y\right)\wedge \left\{B\right\}\cap Y=\varnothing \right)\to \left(\left\{A\right\}\cup X\right)\preccurlyeq \left(\left\{B\right\}\cup Y\right)$$
87	79 80 85 86	syl21anc	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge X\preccurlyeq Y\right)\to \left(\left\{A\right\}\cup X\right)\preccurlyeq \left(\left\{B\right\}\cup Y\right)$$
88	75 87	impbida	$$⊢\left(\neg A\in X\wedge \neg B\in Y\right)\to \left(\left(\left\{A\right\}\cup X\right)\preccurlyeq \left(\left\{B\right\}\cup Y\right)\leftrightarrow X\preccurlyeq Y\right)$$