undom

Description: Dominance law for union. Proposition 4.24(a) of Mendelson p. 257. (Contributed by NM, 3-Sep-2004) (Revised by Mario Carneiro, 26-Apr-2015) Avoid ax-pow . (Revised by BTernaryTau, 4-Dec-2024)

		Ref	Expression
	Assertion	undom	$⊢ ((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \to (A \cup C) ≼ (B \cup D)$

Proof

Step	Hyp	Ref	Expression
1		undif2	$⊢ A \cup (C ∖ A) = A \cup C$
2		reldom	$⊢ Rel ≼$
3	2	brrelex2i	$⊢ A ≼ B \to B \in V$
4	2	brrelex2i	$⊢ C ≼ D \to D \in V$
5		unexg	$⊢ (B \in V \land D \in V) \to B \cup D \in V$
6	3 4 5	syl2an	$⊢ (A ≼ B \land C ≼ D) \to B \cup D \in V$
7	6	adantr	$⊢ ((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \to B \cup D \in V$
8		brdomi	$⊢ A ≼ B \to \exists x x : A \underset{1-1}{⟶} B$
9		brdomi	$⊢ C ≼ D \to \exists y y : C \underset{1-1}{⟶} D$
10		exdistrv	$⊢ \exists x \exists y (x : A \underset{1-1}{⟶} B \land y : C \underset{1-1}{⟶} D) \leftrightarrow (\exists x x : A \underset{1-1}{⟶} B \land \exists y y : C \underset{1-1}{⟶} D)$
11		disjdif	$⊢ A \cap (C ∖ A) = \emptyset$
12		difss	$⊢ C ∖ A \subseteq C$
13		f1ssres	$⊢ (y : C \underset{1-1}{⟶} D \land C ∖ A \subseteq C) \to ({y ↾}_{(C ∖ A)}) : C ∖ A \underset{1-1}{⟶} D$
14	12 13	mpan2	$⊢ y : C \underset{1-1}{⟶} D \to ({y ↾}_{(C ∖ A)}) : C ∖ A \underset{1-1}{⟶} D$
15		f1un	$⊢ ((x : A \underset{1-1}{⟶} B \land ({y ↾}_{(C ∖ A)}) : C ∖ A \underset{1-1}{⟶} D) \land (A \cap (C ∖ A) = \emptyset \land B \cap D = \emptyset)) \to (x \cup ({y ↾}_{(C ∖ A)})) : A \cup (C ∖ A) \underset{1-1}{⟶} B \cup D$
16	14 15	sylanl2	$⊢ ((x : A \underset{1-1}{⟶} B \land y : C \underset{1-1}{⟶} D) \land (A \cap (C ∖ A) = \emptyset \land B \cap D = \emptyset)) \to (x \cup ({y ↾}_{(C ∖ A)})) : A \cup (C ∖ A) \underset{1-1}{⟶} B \cup D$
17	11 16	mpanr1	$⊢ ((x : A \underset{1-1}{⟶} B \land y : C \underset{1-1}{⟶} D) \land B \cap D = \emptyset) \to (x \cup ({y ↾}_{(C ∖ A)})) : A \cup (C ∖ A) \underset{1-1}{⟶} B \cup D$
18		vex	$⊢ x \in V$
19		vex	$⊢ y \in V$
20	19	resex	$⊢ {y ↾}_{(C ∖ A)} \in V$
21	18 20	unex	$⊢ x \cup ({y ↾}_{(C ∖ A)}) \in V$
22		f1dom3g	$⊢ (x \cup ({y ↾}_{(C ∖ A)}) \in V \land B \cup D \in V \land (x \cup ({y ↾}_{(C ∖ A)})) : A \cup (C ∖ A) \underset{1-1}{⟶} B \cup D) \to (A \cup (C ∖ A)) ≼ (B \cup D)$
23	21 22	mp3an1	$⊢ (B \cup D \in V \land (x \cup ({y ↾}_{(C ∖ A)})) : A \cup (C ∖ A) \underset{1-1}{⟶} B \cup D) \to (A \cup (C ∖ A)) ≼ (B \cup D)$
24	23	expcom	$⊢ (x \cup ({y ↾}_{(C ∖ A)})) : A \cup (C ∖ A) \underset{1-1}{⟶} B \cup D \to (B \cup D \in V \to (A \cup (C ∖ A)) ≼ (B \cup D))$
25	17 24	syl	$⊢ ((x : A \underset{1-1}{⟶} B \land y : C \underset{1-1}{⟶} D) \land B \cap D = \emptyset) \to (B \cup D \in V \to (A \cup (C ∖ A)) ≼ (B \cup D))$
26	25	ex	$⊢ (x : A \underset{1-1}{⟶} B \land y : C \underset{1-1}{⟶} D) \to (B \cap D = \emptyset \to (B \cup D \in V \to (A \cup (C ∖ A)) ≼ (B \cup D)))$
27	26	exlimivv	$⊢ \exists x \exists y (x : A \underset{1-1}{⟶} B \land y : C \underset{1-1}{⟶} D) \to (B \cap D = \emptyset \to (B \cup D \in V \to (A \cup (C ∖ A)) ≼ (B \cup D)))$
28	10 27	sylbir	$⊢ (\exists x x : A \underset{1-1}{⟶} B \land \exists y y : C \underset{1-1}{⟶} D) \to (B \cap D = \emptyset \to (B \cup D \in V \to (A \cup (C ∖ A)) ≼ (B \cup D)))$
29	8 9 28	syl2an	$⊢ (A ≼ B \land C ≼ D) \to (B \cap D = \emptyset \to (B \cup D \in V \to (A \cup (C ∖ A)) ≼ (B \cup D)))$
30	29	imp	$⊢ ((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \to (B \cup D \in V \to (A \cup (C ∖ A)) ≼ (B \cup D))$
31	7 30	mpd	$⊢ ((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \to (A \cup (C ∖ A)) ≼ (B \cup D)$
32	1 31	eqbrtrrid	$⊢ ((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \to (A \cup C) ≼ (B \cup D)$

Metamath Proof Explorer

Theorem undom

Proof