unxpwdom

Description: If a Cartesian product is dominated by a union, then the base set is either weakly dominated by one factor of the union or dominated by the other. Extracted from Lemma 2.3 of KanamoriPincus p. 420. (Contributed by Mario Carneiro, 15-May-2015)

		Ref	Expression
	Assertion	unxpwdom	$⊢ (A \times A) ≼ (B \cup C) \to (A ≼^{*} B \lor A ≼ C)$

Proof

Step	Hyp	Ref	Expression
1		reldom	$⊢ Rel ≼$
2	1	brrelex2i	$⊢ (A \times A) ≼ (B \cup C) \to B \cup C \in V$
3		domeng	$⊢ B \cup C \in V \to ((A \times A) ≼ (B \cup C) \leftrightarrow \exists x ((A \times A) \approx x \land x \subseteq B \cup C))$
4	2 3	syl	$⊢ (A \times A) ≼ (B \cup C) \to ((A \times A) ≼ (B \cup C) \leftrightarrow \exists x ((A \times A) \approx x \land x \subseteq B \cup C))$
5	4	ibi	$⊢ (A \times A) ≼ (B \cup C) \to \exists x ((A \times A) \approx x \land x \subseteq B \cup C)$
6		simprl	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to (A \times A) \approx x$
7		indi	$⊢ x \cap (B \cup C) = (x \cap B) \cup (x \cap C)$
8		simprr	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to x \subseteq B \cup C$
9		df-ss	$⊢ x \subseteq B \cup C \leftrightarrow x \cap (B \cup C) = x$
10	8 9	sylib	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to x \cap (B \cup C) = x$
11	7 10	eqtr3id	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to (x \cap B) \cup (x \cap C) = x$
12	6 11	breqtrrd	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to (A \times A) \approx ((x \cap B) \cup (x \cap C))$
13		unxpwdom2	$⊢ (A \times A) \approx ((x \cap B) \cup (x \cap C)) \to (A ≼^{*} (x \cap B) \lor A ≼ (x \cap C))$
14	12 13	syl	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to (A ≼^{*} (x \cap B) \lor A ≼ (x \cap C))$
15		ssun1	$⊢ B \subseteq B \cup C$
16	2	adantr	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to B \cup C \in V$
17		ssexg	$⊢ (B \subseteq B \cup C \land B \cup C \in V) \to B \in V$
18	15 16 17	sylancr	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to B \in V$
19		inss2	$⊢ x \cap B \subseteq B$
20		ssdomg	$⊢ B \in V \to (x \cap B \subseteq B \to (x \cap B) ≼ B)$
21	18 19 20	mpisyl	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to (x \cap B) ≼ B$
22		domwdom	$⊢ (x \cap B) ≼ B \to (x \cap B) ≼^{*} B$
23	21 22	syl	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to (x \cap B) ≼^{*} B$
24		wdomtr	$⊢ (A ≼^{} (x \cap B) \land (x \cap B) ≼^{} B) \to A ≼^{*} B$
25	24	expcom	$⊢ (x \cap B) ≼^{} B \to (A ≼^{} (x \cap B) \to A ≼^{*} B)$
26	23 25	syl	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to (A ≼^{} (x \cap B) \to A ≼^{} B)$
27		ssun2	$⊢ C \subseteq B \cup C$
28		ssexg	$⊢ (C \subseteq B \cup C \land B \cup C \in V) \to C \in V$
29	27 16 28	sylancr	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to C \in V$
30		inss2	$⊢ x \cap C \subseteq C$
31		ssdomg	$⊢ C \in V \to (x \cap C \subseteq C \to (x \cap C) ≼ C)$
32	29 30 31	mpisyl	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to (x \cap C) ≼ C$
33		domtr	$⊢ (A ≼ (x \cap C) \land (x \cap C) ≼ C) \to A ≼ C$
34	33	expcom	$⊢ (x \cap C) ≼ C \to (A ≼ (x \cap C) \to A ≼ C)$
35	32 34	syl	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to (A ≼ (x \cap C) \to A ≼ C)$
36	26 35	orim12d	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to ((A ≼^{} (x \cap B) \lor A ≼ (x \cap C)) \to (A ≼^{} B \lor A ≼ C))$
37	14 36	mpd	$⊢ ((A \times A) ≼ (B \cup C) \land ((A \times A) \approx x \land x \subseteq B \cup C)) \to (A ≼^{*} B \lor A ≼ C)$
38	5 37	exlimddv	$⊢ (A \times A) ≼ (B \cup C) \to (A ≼^{*} B \lor A ≼ C)$

Metamath Proof Explorer

Theorem unxpwdom

Proof