Metamath Proof Explorer

Theorem xpdom3

Description: A set is dominated by its Cartesian product with a nonempty set. Exercise 6 of Suppes p. 98. (Contributed by NM, 27-Jul-2004) (Revised by Mario Carneiro, 29-Apr-2015)

		Ref	Expression
	Assertion	xpdom3	$⊢ (A \in V \land B \in W \land B \neq \emptyset) \to A ≼ (A \times B)$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ B \neq \emptyset \leftrightarrow \exists x x \in B$
2		xpsneng	$⊢ (A \in V \land x \in B) \to (A \times \{x\}) \approx A$
3	2	3adant2	$⊢ (A \in V \land B \in W \land x \in B) \to (A \times \{x\}) \approx A$
4	3	ensymd	$⊢ (A \in V \land B \in W \land x \in B) \to A \approx (A \times \{x\})$
5		xpexg	$⊢ (A \in V \land B \in W) \to A \times B \in V$
6	5	3adant3	$⊢ (A \in V \land B \in W \land x \in B) \to A \times B \in V$
7		simp3	$⊢ (A \in V \land B \in W \land x \in B) \to x \in B$
8	7	snssd	$⊢ (A \in V \land B \in W \land x \in B) \to \{x\} \subseteq B$
9		xpss2	$⊢ \{x\} \subseteq B \to A \times \{x\} \subseteq A \times B$
10	8 9	syl	$⊢ (A \in V \land B \in W \land x \in B) \to A \times \{x\} \subseteq A \times B$
11		ssdomg	$⊢ A \times B \in V \to (A \times \{x\} \subseteq A \times B \to (A \times \{x\}) ≼ (A \times B))$
12	6 10 11	sylc	$⊢ (A \in V \land B \in W \land x \in B) \to (A \times \{x\}) ≼ (A \times B)$
13		endomtr	$⊢ (A \approx (A \times \{x\}) \land (A \times \{x\}) ≼ (A \times B)) \to A ≼ (A \times B)$
14	4 12 13	syl2anc	$⊢ (A \in V \land B \in W \land x \in B) \to A ≼ (A \times B)$
15	14	3expia	$⊢ (A \in V \land B \in W) \to (x \in B \to A ≼ (A \times B))$
16	15	exlimdv	$⊢ (A \in V \land B \in W) \to (\exists x x \in B \to A ≼ (A \times B))$
17	1 16	biimtrid	$⊢ (A \in V \land B \in W) \to (B \neq \emptyset \to A ≼ (A \times B))$
18	17	3impia	$⊢ (A \in V \land B \in W \land B \neq \emptyset) \to A ≼ (A \times B)$