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)

		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		reldom	$⊢ Rel ≼$
2	1	brrelex2i	$⊢ A ≼ B \to B \in V$
3		domeng	$⊢ B \in V \to (A ≼ B \leftrightarrow \exists x (A \approx x \land x \subseteq B))$
4	2 3	syl	$⊢ A ≼ B \to (A ≼ B \leftrightarrow \exists x (A \approx x \land x \subseteq B))$
5	4	ibi	$⊢ A ≼ B \to \exists x (A \approx x \land x \subseteq B)$
6	1	brrelex1i	$⊢ C ≼ D \to C \in V$
7		difss	$⊢ C ∖ A \subseteq C$
8		ssdomg	$⊢ C \in V \to (C ∖ A \subseteq C \to (C ∖ A) ≼ C)$
9	6 7 8	mpisyl	$⊢ C ≼ D \to (C ∖ A) ≼ C$
10		domtr	$⊢ ((C ∖ A) ≼ C \land C ≼ D) \to (C ∖ A) ≼ D$
11	9 10	mpancom	$⊢ C ≼ D \to (C ∖ A) ≼ D$
12	1	brrelex2i	$⊢ (C ∖ A) ≼ D \to D \in V$
13		domeng	$⊢ D \in V \to ((C ∖ A) ≼ D \leftrightarrow \exists y ((C ∖ A) \approx y \land y \subseteq D))$
14	12 13	syl	$⊢ (C ∖ A) ≼ D \to ((C ∖ A) ≼ D \leftrightarrow \exists y ((C ∖ A) \approx y \land y \subseteq D))$
15	14	ibi	$⊢ (C ∖ A) ≼ D \to \exists y ((C ∖ A) \approx y \land y \subseteq D)$
16	11 15	syl	$⊢ C ≼ D \to \exists y ((C ∖ A) \approx y \land y \subseteq D)$
17	5 16	anim12i	$⊢ (A ≼ B \land C ≼ D) \to (\exists x (A \approx x \land x \subseteq B) \land \exists y ((C ∖ A) \approx y \land y \subseteq D))$
18	17	adantr	$⊢ ((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \to (\exists x (A \approx x \land x \subseteq B) \land \exists y ((C ∖ A) \approx y \land y \subseteq D))$
19		exdistrv	$⊢ \exists x \exists y ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D)) \leftrightarrow (\exists x (A \approx x \land x \subseteq B) \land \exists y ((C ∖ A) \approx y \land y \subseteq D))$
20		simprll	$⊢ (((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \land ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D))) \to A \approx x$
21		simprrl	$⊢ (((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \land ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D))) \to (C ∖ A) \approx y$
22		disjdif	$⊢ A \cap (C ∖ A) = \emptyset$
23	22	a1i	$⊢ (((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \land ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D))) \to A \cap (C ∖ A) = \emptyset$
24		ss2in	$⊢ (x \subseteq B \land y \subseteq D) \to x \cap y \subseteq B \cap D$
25	24	ad2ant2l	$⊢ ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D)) \to x \cap y \subseteq B \cap D$
26	25	adantl	$⊢ (((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \land ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D))) \to x \cap y \subseteq B \cap D$
27		simplr	$⊢ (((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \land ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D))) \to B \cap D = \emptyset$
28		sseq0	$⊢ (x \cap y \subseteq B \cap D \land B \cap D = \emptyset) \to x \cap y = \emptyset$
29	26 27 28	syl2anc	$⊢ (((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \land ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D))) \to x \cap y = \emptyset$
30		undif2	$⊢ A \cup (C ∖ A) = A \cup C$
31		unen	$⊢ ((A \approx x \land (C ∖ A) \approx y) \land (A \cap (C ∖ A) = \emptyset \land x \cap y = \emptyset)) \to (A \cup (C ∖ A)) \approx (x \cup y)$
32	30 31	eqbrtrrid	$⊢ ((A \approx x \land (C ∖ A) \approx y) \land (A \cap (C ∖ A) = \emptyset \land x \cap y = \emptyset)) \to (A \cup C) \approx (x \cup y)$
33	20 21 23 29 32	syl22anc	$⊢ (((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \land ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D))) \to (A \cup C) \approx (x \cup y)$
34	2	ad3antrrr	$⊢ (((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \land ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D))) \to B \in V$
35	1	brrelex2i	$⊢ C ≼ D \to D \in V$
36	35	ad3antlr	$⊢ (((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \land ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D))) \to D \in V$
37		unexg	$⊢ (B \in V \land D \in V) \to B \cup D \in V$
38	34 36 37	syl2anc	$⊢ (((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \land ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D))) \to B \cup D \in V$
39		unss12	$⊢ (x \subseteq B \land y \subseteq D) \to x \cup y \subseteq B \cup D$
40	39	ad2ant2l	$⊢ ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D)) \to x \cup y \subseteq B \cup D$
41	40	adantl	$⊢ (((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \land ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D))) \to x \cup y \subseteq B \cup D$
42		ssdomg	$⊢ B \cup D \in V \to (x \cup y \subseteq B \cup D \to (x \cup y) ≼ (B \cup D))$
43	38 41 42	sylc	$⊢ (((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \land ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D))) \to (x \cup y) ≼ (B \cup D)$
44		endomtr	$⊢ ((A \cup C) \approx (x \cup y) \land (x \cup y) ≼ (B \cup D)) \to (A \cup C) ≼ (B \cup D)$
45	33 43 44	syl2anc	$⊢ (((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \land ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D))) \to (A \cup C) ≼ (B \cup D)$
46	45	ex	$⊢ ((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \to (((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D)) \to (A \cup C) ≼ (B \cup D))$
47	46	exlimdvv	$⊢ ((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \to (\exists x \exists y ((A \approx x \land x \subseteq B) \land ((C ∖ A) \approx y \land y \subseteq D)) \to (A \cup C) ≼ (B \cup D))$
48	19 47	syl5bir	$⊢ ((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \to ((\exists x (A \approx x \land x \subseteq B) \land \exists y ((C ∖ A) \approx y \land y \subseteq D)) \to (A \cup C) ≼ (B \cup D))$
49	18 48	mpd	$⊢ ((A ≼ B \land C ≼ D) \land B \cap D = \emptyset) \to (A \cup C) ≼ (B \cup D)$

Metamath Proof Explorer

Theorem undom

Proof