domunfican

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

		Ref	Expression
	Assertion	domunfican	$⊢ ((A \in Fin \land B \approx A) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((A \cup X) ≼ (B \cup Y) \leftrightarrow X ≼ Y)$

Proof

Step	Hyp	Ref	Expression
1		ensym	$⊢ B \approx A \to A \approx B$
2		bren	$⊢ A \approx B \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} B$
3	1 2	sylib	$⊢ B \approx A \to \exists f f : A \underset{1-1 onto}{⟶} B$
4		ssid	$⊢ A \subseteq A$
5		sseq1	$⊢ a = \emptyset \to (a \subseteq A \leftrightarrow \emptyset \subseteq A)$
6	5	anbi1d	$⊢ a = \emptyset \to ((a \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \leftrightarrow (\emptyset \subseteq A \land f : A \underset{1-1 onto}{⟶} B))$
7	6	anbi1d	$⊢ a = \emptyset \to (((a \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \leftrightarrow ((\emptyset \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)))$
8		uneq1	$⊢ a = \emptyset \to a \cup X = \emptyset \cup X$
9		imaeq2	$⊢ a = \emptyset \to f [a] = f [\emptyset]$
10	9	uneq1d	$⊢ a = \emptyset \to f [a] \cup Y = f [\emptyset] \cup Y$
11	8 10	breq12d	$⊢ a = \emptyset \to ((a \cup X) ≼ (f [a] \cup Y) \leftrightarrow (\emptyset \cup X) ≼ (f [\emptyset] \cup Y))$
12	11	bibi1d	$⊢ a = \emptyset \to (((a \cup X) ≼ (f [a] \cup Y) \leftrightarrow X ≼ Y) \leftrightarrow ((\emptyset \cup X) ≼ (f [\emptyset] \cup Y) \leftrightarrow X ≼ Y))$
13	7 12	imbi12d	$⊢ a = \emptyset \to ((((a \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((a \cup X) ≼ (f [a] \cup Y) \leftrightarrow X ≼ Y)) \leftrightarrow (((\emptyset \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((\emptyset \cup X) ≼ (f [\emptyset] \cup Y) \leftrightarrow X ≼ Y)))$
14		sseq1	$⊢ a = b \to (a \subseteq A \leftrightarrow b \subseteq A)$
15	14	anbi1d	$⊢ a = b \to ((a \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \leftrightarrow (b \subseteq A \land f : A \underset{1-1 onto}{⟶} B))$
16	15	anbi1d	$⊢ a = b \to (((a \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \leftrightarrow ((b \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)))$
17		uneq1	$⊢ a = b \to a \cup X = b \cup X$
18		imaeq2	$⊢ a = b \to f [a] = f [b]$
19	18	uneq1d	$⊢ a = b \to f [a] \cup Y = f [b] \cup Y$
20	17 19	breq12d	$⊢ a = b \to ((a \cup X) ≼ (f [a] \cup Y) \leftrightarrow (b \cup X) ≼ (f [b] \cup Y))$
21	20	bibi1d	$⊢ a = b \to (((a \cup X) ≼ (f [a] \cup Y) \leftrightarrow X ≼ Y) \leftrightarrow ((b \cup X) ≼ (f [b] \cup Y) \leftrightarrow X ≼ Y))$
22	16 21	imbi12d	$⊢ a = b \to ((((a \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((a \cup X) ≼ (f [a] \cup Y) \leftrightarrow X ≼ Y)) \leftrightarrow (((b \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((b \cup X) ≼ (f [b] \cup Y) \leftrightarrow X ≼ Y)))$
23		sseq1	$⊢ a = b \cup \{c\} \to (a \subseteq A \leftrightarrow b \cup \{c\} \subseteq A)$
24	23	anbi1d	$⊢ a = b \cup \{c\} \to ((a \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \leftrightarrow (b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B))$
25	24	anbi1d	$⊢ a = b \cup \{c\} \to (((a \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \leftrightarrow ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)))$
26		uneq1	$⊢ a = b \cup \{c\} \to a \cup X = (b \cup \{c\}) \cup X$
27		imaeq2	$⊢ a = b \cup \{c\} \to f [a] = f [b \cup \{c\}]$
28	27	uneq1d	$⊢ a = b \cup \{c\} \to f [a] \cup Y = f [b \cup \{c\}] \cup Y$
29	26 28	breq12d	$⊢ a = b \cup \{c\} \to ((a \cup X) ≼ (f [a] \cup Y) \leftrightarrow ((b \cup \{c\}) \cup X) ≼ (f [b \cup \{c\}] \cup Y))$
30	29	bibi1d	$⊢ a = b \cup \{c\} \to (((a \cup X) ≼ (f [a] \cup Y) \leftrightarrow X ≼ Y) \leftrightarrow (((b \cup \{c\}) \cup X) ≼ (f [b \cup \{c\}] \cup Y) \leftrightarrow X ≼ Y))$
31	25 30	imbi12d	$⊢ a = b \cup \{c\} \to ((((a \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((a \cup X) ≼ (f [a] \cup Y) \leftrightarrow X ≼ Y)) \leftrightarrow (((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to (((b \cup \{c\}) \cup X) ≼ (f [b \cup \{c\}] \cup Y) \leftrightarrow X ≼ Y)))$
32		sseq1	$⊢ a = A \to (a \subseteq A \leftrightarrow A \subseteq A)$
33	32	anbi1d	$⊢ a = A \to ((a \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \leftrightarrow (A \subseteq A \land f : A \underset{1-1 onto}{⟶} B))$
34	33	anbi1d	$⊢ a = A \to (((a \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \leftrightarrow ((A \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)))$
35		uneq1	$⊢ a = A \to a \cup X = A \cup X$
36		imaeq2	$⊢ a = A \to f [a] = f [A]$
37	36	uneq1d	$⊢ a = A \to f [a] \cup Y = f [A] \cup Y$
38	35 37	breq12d	$⊢ a = A \to ((a \cup X) ≼ (f [a] \cup Y) \leftrightarrow (A \cup X) ≼ (f [A] \cup Y))$
39	38	bibi1d	$⊢ a = A \to (((a \cup X) ≼ (f [a] \cup Y) \leftrightarrow X ≼ Y) \leftrightarrow ((A \cup X) ≼ (f [A] \cup Y) \leftrightarrow X ≼ Y))$
40	34 39	imbi12d	$⊢ a = A \to ((((a \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((a \cup X) ≼ (f [a] \cup Y) \leftrightarrow X ≼ Y)) \leftrightarrow (((A \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((A \cup X) ≼ (f [A] \cup Y) \leftrightarrow X ≼ Y)))$
41		uncom	$⊢ \emptyset \cup X = X \cup \emptyset$
42		un0	$⊢ X \cup \emptyset = X$
43	41 42	eqtri	$⊢ \emptyset \cup X = X$
44		ima0	$⊢ f [\emptyset] = \emptyset$
45	44	uneq1i	$⊢ f [\emptyset] \cup Y = \emptyset \cup Y$
46		uncom	$⊢ \emptyset \cup Y = Y \cup \emptyset$
47		un0	$⊢ Y \cup \emptyset = Y$
48	46 47	eqtri	$⊢ \emptyset \cup Y = Y$
49	45 48	eqtri	$⊢ f [\emptyset] \cup Y = Y$
50	43 49	breq12i	$⊢ (\emptyset \cup X) ≼ (f [\emptyset] \cup Y) \leftrightarrow X ≼ Y$
51	50	a1i	$⊢ ((\emptyset \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((\emptyset \cup X) ≼ (f [\emptyset] \cup Y) \leftrightarrow X ≼ Y)$
52		ssun1	$⊢ b \subseteq b \cup \{c\}$
53		sstr2	$⊢ b \subseteq b \cup \{c\} \to (b \cup \{c\} \subseteq A \to b \subseteq A)$
54	52 53	ax-mp	$⊢ b \cup \{c\} \subseteq A \to b \subseteq A$
55	54	anim1i	$⊢ (b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \to (b \subseteq A \land f : A \underset{1-1 onto}{⟶} B)$
56	55	anim1i	$⊢ ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((b \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))$
57	56	imim1i	$⊢ (((b \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((b \cup X) ≼ (f [b] \cup Y) \leftrightarrow X ≼ Y)) \to (((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((b \cup X) ≼ (f [b] \cup Y) \leftrightarrow X ≼ Y))$
58		uncom	$⊢ b \cup \{c\} = \{c\} \cup b$
59	58	uneq1i	$⊢ (b \cup \{c\}) \cup X = (\{c\} \cup b) \cup X$
60		unass	$⊢ (\{c\} \cup b) \cup X = \{c\} \cup (b \cup X)$
61	59 60	eqtri	$⊢ (b \cup \{c\}) \cup X = \{c\} \cup (b \cup X)$
62	61	a1i	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to (b \cup \{c\}) \cup X = \{c\} \cup (b \cup X)$
63		imaundi	$⊢ f [b \cup \{c\}] = f [b] \cup f [\{c\}]$
64		simprlr	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to f : A \underset{1-1 onto}{⟶} B$
65		f1ofn	$⊢ f : A \underset{1-1 onto}{⟶} B \to f Fn A$
66	64 65	syl	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to f Fn A$
67		ssun2	$⊢ \{c\} \subseteq b \cup \{c\}$
68		sstr2	$⊢ \{c\} \subseteq b \cup \{c\} \to (b \cup \{c\} \subseteq A \to \{c\} \subseteq A)$
69	67 68	ax-mp	$⊢ b \cup \{c\} \subseteq A \to \{c\} \subseteq A$
70		vex	$⊢ c \in V$
71	70	snss	$⊢ c \in A \leftrightarrow \{c\} \subseteq A$
72	69 71	sylibr	$⊢ b \cup \{c\} \subseteq A \to c \in A$
73	72	adantr	$⊢ (b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \to c \in A$
74	73	ad2antrl	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to c \in A$
75		fnsnfv	$⊢ (f Fn A \land c \in A) \to \{f (c)\} = f [\{c\}]$
76	66 74 75	syl2anc	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to \{f (c)\} = f [\{c\}]$
77	76	eqcomd	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to f [\{c\}] = \{f (c)\}$
78	77	uneq2d	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to f [b] \cup f [\{c\}] = f [b] \cup \{f (c)\}$
79	63 78	eqtrid	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to f [b \cup \{c\}] = f [b] \cup \{f (c)\}$
80	79	uneq1d	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to f [b \cup \{c\}] \cup Y = (f [b] \cup \{f (c)\}) \cup Y$
81		uncom	$⊢ f [b] \cup \{f (c)\} = \{f (c)\} \cup f [b]$
82	81	uneq1i	$⊢ (f [b] \cup \{f (c)\}) \cup Y = (\{f (c)\} \cup f [b]) \cup Y$
83		unass	$⊢ (\{f (c)\} \cup f [b]) \cup Y = \{f (c)\} \cup (f [b] \cup Y)$
84	82 83	eqtri	$⊢ (f [b] \cup \{f (c)\}) \cup Y = \{f (c)\} \cup (f [b] \cup Y)$
85	80 84	eqtrdi	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to f [b \cup \{c\}] \cup Y = \{f (c)\} \cup (f [b] \cup Y)$
86	62 85	breq12d	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to (((b \cup \{c\}) \cup X) ≼ (f [b \cup \{c\}] \cup Y) \leftrightarrow (\{c\} \cup (b \cup X)) ≼ (\{f (c)\} \cup (f [b] \cup Y)))$
87		simplr	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to \neg c \in b$
88		incom	$⊢ X \cap A = A \cap X$
89		simprrl	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to A \cap X = \emptyset$
90	88 89	eqtrid	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to X \cap A = \emptyset$
91		minel	$⊢ (c \in A \land X \cap A = \emptyset) \to \neg c \in X$
92	74 90 91	syl2anc	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to \neg c \in X$
93		ioran	$⊢ \neg (c \in b \lor c \in X) \leftrightarrow (\neg c \in b \land \neg c \in X)$
94		elun	$⊢ c \in (b \cup X) \leftrightarrow (c \in b \lor c \in X)$
95	93 94	xchnxbir	$⊢ \neg c \in (b \cup X) \leftrightarrow (\neg c \in b \land \neg c \in X)$
96	87 92 95	sylanbrc	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to \neg c \in (b \cup X)$
97		simplr	$⊢ ((b \in Fin \land \neg c \in b) \land (b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B)) \to \neg c \in b$
98		f1of1	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A \underset{1-1}{⟶} B$
99	98	adantl	$⊢ (b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \to f : A \underset{1-1}{⟶} B$
100	54	adantr	$⊢ (b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \to b \subseteq A$
101		f1elima	$⊢ (f : A \underset{1-1}{⟶} B \land c \in A \land b \subseteq A) \to (f (c) \in f [b] \leftrightarrow c \in b)$
102	99 73 100 101	syl3anc	$⊢ (b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \to (f (c) \in f [b] \leftrightarrow c \in b)$
103	102	biimpd	$⊢ (b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \to (f (c) \in f [b] \to c \in b)$
104	103	adantl	$⊢ ((b \in Fin \land \neg c \in b) \land (b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B)) \to (f (c) \in f [b] \to c \in b)$
105	97 104	mtod	$⊢ ((b \in Fin \land \neg c \in b) \land (b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B)) \to \neg f (c) \in f [b]$
106	105	adantrr	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to \neg f (c) \in f [b]$
107		f1of	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A ⟶ B$
108	64 107	syl	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to f : A ⟶ B$
109	108 74	ffvelrnd	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to f (c) \in B$
110		incom	$⊢ Y \cap B = B \cap Y$
111		simprrr	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to B \cap Y = \emptyset$
112	110 111	eqtrid	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to Y \cap B = \emptyset$
113		minel	$⊢ (f (c) \in B \land Y \cap B = \emptyset) \to \neg f (c) \in Y$
114	109 112 113	syl2anc	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to \neg f (c) \in Y$
115		ioran	$⊢ \neg (f (c) \in f [b] \lor f (c) \in Y) \leftrightarrow (\neg f (c) \in f [b] \land \neg f (c) \in Y)$
116		elun	$⊢ f (c) \in (f [b] \cup Y) \leftrightarrow (f (c) \in f [b] \lor f (c) \in Y)$
117	115 116	xchnxbir	$⊢ \neg f (c) \in (f [b] \cup Y) \leftrightarrow (\neg f (c) \in f [b] \land \neg f (c) \in Y)$
118	106 114 117	sylanbrc	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to \neg f (c) \in (f [b] \cup Y)$
119		fvex	$⊢ f (c) \in V$
120	70 119	domunsncan	$⊢ (\neg c \in (b \cup X) \land \neg f (c) \in (f [b] \cup Y)) \to ((\{c\} \cup (b \cup X)) ≼ (\{f (c)\} \cup (f [b] \cup Y)) \leftrightarrow (b \cup X) ≼ (f [b] \cup Y))$
121	96 118 120	syl2anc	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to ((\{c\} \cup (b \cup X)) ≼ (\{f (c)\} \cup (f [b] \cup Y)) \leftrightarrow (b \cup X) ≼ (f [b] \cup Y))$
122	86 121	bitrd	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to (((b \cup \{c\}) \cup X) ≼ (f [b \cup \{c\}] \cup Y) \leftrightarrow (b \cup X) ≼ (f [b] \cup Y))$
123		bitr	$⊢ ((((b \cup \{c\}) \cup X) ≼ (f [b \cup \{c\}] \cup Y) \leftrightarrow (b \cup X) ≼ (f [b] \cup Y)) \land ((b \cup X) ≼ (f [b] \cup Y) \leftrightarrow X ≼ Y)) \to (((b \cup \{c\}) \cup X) ≼ (f [b \cup \{c\}] \cup Y) \leftrightarrow X ≼ Y)$
124	123	ex	$⊢ (((b \cup \{c\}) \cup X) ≼ (f [b \cup \{c\}] \cup Y) \leftrightarrow (b \cup X) ≼ (f [b] \cup Y)) \to (((b \cup X) ≼ (f [b] \cup Y) \leftrightarrow X ≼ Y) \to (((b \cup \{c\}) \cup X) ≼ (f [b \cup \{c\}] \cup Y) \leftrightarrow X ≼ Y))$
125	122 124	syl	$⊢ ((b \in Fin \land \neg c \in b) \land ((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset))) \to (((b \cup X) ≼ (f [b] \cup Y) \leftrightarrow X ≼ Y) \to (((b \cup \{c\}) \cup X) ≼ (f [b \cup \{c\}] \cup Y) \leftrightarrow X ≼ Y))$
126	125	ex	$⊢ (b \in Fin \land \neg c \in b) \to (((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to (((b \cup X) ≼ (f [b] \cup Y) \leftrightarrow X ≼ Y) \to (((b \cup \{c\}) \cup X) ≼ (f [b \cup \{c\}] \cup Y) \leftrightarrow X ≼ Y)))$
127	126	a2d	$⊢ (b \in Fin \land \neg c \in b) \to ((((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((b \cup X) ≼ (f [b] \cup Y) \leftrightarrow X ≼ Y)) \to (((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to (((b \cup \{c\}) \cup X) ≼ (f [b \cup \{c\}] \cup Y) \leftrightarrow X ≼ Y)))$
128	57 127	syl5	$⊢ (b \in Fin \land \neg c \in b) \to ((((b \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((b \cup X) ≼ (f [b] \cup Y) \leftrightarrow X ≼ Y)) \to (((b \cup \{c\} \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to (((b \cup \{c\}) \cup X) ≼ (f [b \cup \{c\}] \cup Y) \leftrightarrow X ≼ Y)))$
129	13 22 31 40 51 128	findcard2s	$⊢ A \in Fin \to (((A \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((A \cup X) ≼ (f [A] \cup Y) \leftrightarrow X ≼ Y))$
130	129	expd	$⊢ A \in Fin \to ((A \subseteq A \land f : A \underset{1-1 onto}{⟶} B) \to ((A \cap X = \emptyset \land B \cap Y = \emptyset) \to ((A \cup X) ≼ (f [A] \cup Y) \leftrightarrow X ≼ Y)))$
131	4 130	mpani	$⊢ A \in Fin \to (f : A \underset{1-1 onto}{⟶} B \to ((A \cap X = \emptyset \land B \cap Y = \emptyset) \to ((A \cup X) ≼ (f [A] \cup Y) \leftrightarrow X ≼ Y)))$
132	131	3imp	$⊢ (A \in Fin \land f : A \underset{1-1 onto}{⟶} B \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((A \cup X) ≼ (f [A] \cup Y) \leftrightarrow X ≼ Y)$
133		f1ofo	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A \underset{onto}{⟶} B$
134		foima	$⊢ f : A \underset{onto}{⟶} B \to f [A] = B$
135	133 134	syl	$⊢ f : A \underset{1-1 onto}{⟶} B \to f [A] = B$
136	135	uneq1d	$⊢ f : A \underset{1-1 onto}{⟶} B \to f [A] \cup Y = B \cup Y$
137	136	breq2d	$⊢ f : A \underset{1-1 onto}{⟶} B \to ((A \cup X) ≼ (f [A] \cup Y) \leftrightarrow (A \cup X) ≼ (B \cup Y))$
138	137	bibi1d	$⊢ f : A \underset{1-1 onto}{⟶} B \to (((A \cup X) ≼ (f [A] \cup Y) \leftrightarrow X ≼ Y) \leftrightarrow ((A \cup X) ≼ (B \cup Y) \leftrightarrow X ≼ Y))$
139	138	3ad2ant2	$⊢ (A \in Fin \land f : A \underset{1-1 onto}{⟶} B \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to (((A \cup X) ≼ (f [A] \cup Y) \leftrightarrow X ≼ Y) \leftrightarrow ((A \cup X) ≼ (B \cup Y) \leftrightarrow X ≼ Y))$
140	132 139	mpbid	$⊢ (A \in Fin \land f : A \underset{1-1 onto}{⟶} B \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((A \cup X) ≼ (B \cup Y) \leftrightarrow X ≼ Y)$
141	140	3exp	$⊢ A \in Fin \to (f : A \underset{1-1 onto}{⟶} B \to ((A \cap X = \emptyset \land B \cap Y = \emptyset) \to ((A \cup X) ≼ (B \cup Y) \leftrightarrow X ≼ Y)))$
142	141	exlimdv	$⊢ A \in Fin \to (\exists f f : A \underset{1-1 onto}{⟶} B \to ((A \cap X = \emptyset \land B \cap Y = \emptyset) \to ((A \cup X) ≼ (B \cup Y) \leftrightarrow X ≼ Y)))$
143	3 142	syl5	$⊢ A \in Fin \to (B \approx A \to ((A \cap X = \emptyset \land B \cap Y = \emptyset) \to ((A \cup X) ≼ (B \cup Y) \leftrightarrow X ≼ Y)))$
144	143	imp31	$⊢ ((A \in Fin \land B \approx A) \land (A \cap X = \emptyset \land B \cap Y = \emptyset)) \to ((A \cup X) ≼ (B \cup Y) \leftrightarrow X ≼ Y)$

Metamath Proof Explorer

Theorem domunfican

Proof