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		difexg	$$⊢\left\{B\right\}\cup Y\in \mathrm{V}\to \left(\left\{B\right\}\cup Y\right)\setminus \left\{f\left(A\right)\right\}\in \mathrm{V}$$
27	25 26	syl	$$⊢\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}$$
28		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$$
29		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$$
30	28 29	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$$
31	30	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$$
32	31	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]$$
33		f1fn	$$⊢f:\left\{A\right\}\cup X\underset{1-1}{⟶}\left\{B\right\}\cup Y\to fFn\left(\left\{A\right\}\cup X\right)$$
34	33	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)$$
35	1	snid	$$⊢A\in \left\{A\right\}$$
36		elun1	$$⊢A\in \left\{A\right\}\to A\in \left(\left\{A\right\}\cup X\right)$$
37	35 36	ax-mp	$$⊢A\in \left(\left\{A\right\}\cup X\right)$$
38		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]$$
39	34 37 38	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]$$
40	39	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]$$
41	32 40	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\}$$
42		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)$$
43	27 41 42	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)$$
44		ffvelrn	$$⊢\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)$$
45	28 37 44	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)$$
46	45	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)$$
47	2	snid	$$⊢B\in \left\{B\right\}$$
48		elun1	$$⊢B\in \left\{B\right\}\to B\in \left(\left\{B\right\}\cup Y\right)$$
49	47 48	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)$$
50		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)$$
51	25 46 49 50	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)$$
52		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)$$
53	43 51 52	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)$$
54	21 53	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)$$
55		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)$$
56	17 54 55	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)$$
57		uncom	$$⊢\left\{A\right\}\cup X=X\cup \left\{A\right\}$$
58	57	difeq1i	$$⊢\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}=\left(X\cup \left\{A\right\}\right)\setminus \left\{A\right\}$$
59		difun2	$$⊢\left(X\cup \left\{A\right\}\right)\setminus \left\{A\right\}=X\setminus \left\{A\right\}$$
60	58 59	eqtri	$$⊢\left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}=X\setminus \left\{A\right\}$$
61		difsn	$$⊢\neg A\in X\to X\setminus \left\{A\right\}=X$$
62	60 61	syl5eq	$$⊢\neg A\in X\to \left(\left\{A\right\}\cup X\right)\setminus \left\{A\right\}=X$$
63	62	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$$
64		uncom	$$⊢\left\{B\right\}\cup Y=Y\cup \left\{B\right\}$$
65	64	difeq1i	$$⊢\left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}=\left(Y\cup \left\{B\right\}\right)\setminus \left\{B\right\}$$
66		difun2	$$⊢\left(Y\cup \left\{B\right\}\right)\setminus \left\{B\right\}=Y\setminus \left\{B\right\}$$
67	65 66	eqtri	$$⊢\left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}=Y\setminus \left\{B\right\}$$
68		difsn	$$⊢\neg B\in Y\to Y\setminus \left\{B\right\}=Y$$
69	67 68	syl5eq	$$⊢\neg B\in Y\to \left(\left\{B\right\}\cup Y\right)\setminus \left\{B\right\}=Y$$
70	69	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$$
71	56 63 70	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$$
72	71	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)$$
73	72	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)$$
74	9 73	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)$$
75	74	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)$$
76	8 75	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$$
77		en2sn	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left\{A\right\}\approx \left\{B\right\}$$
78	1 2 77	mp2an	$$⊢\left\{A\right\}\approx \left\{B\right\}$$
79		endom	$$⊢\left\{A\right\}\approx \left\{B\right\}\to \left\{A\right\}\preccurlyeq \left\{B\right\}$$
80	78 79	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\}$$
81		simpr	$$⊢\left(\left(\neg A\in X\wedge \neg B\in Y\right)\wedge X\preccurlyeq Y\right)\to X\preccurlyeq Y$$
82		incom	$$⊢\left\{B\right\}\cap Y=Y\cap \left\{B\right\}$$
83		disjsn	$$⊢Y\cap \left\{B\right\}=\varnothing \leftrightarrow \neg B\in Y$$
84	83	biimpri	$$⊢\neg B\in Y\to Y\cap \left\{B\right\}=\varnothing$$
85	82 84	syl5eq	$$⊢\neg B\in Y\to \left\{B\right\}\cap Y=\varnothing$$
86	85	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$$
87		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)$$
88	80 81 86 87	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)$$
89	76 88	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)$$