sucxpdom

Description: Cartesian product dominates successor for set with cardinality greater than 1. Proposition 10.38 of TakeutiZaring p. 93 (but generalized to arbitrary sets, not just ordinals). (Contributed by NM, 3-Sep-2004) (Proof shortened by Mario Carneiro, 27-Apr-2015)

		Ref	Expression
	Assertion	sucxpdom	$⊢ 1_{𝑜} ≺ A \to suc A ≼ (A \times A)$

Proof

Step	Hyp	Ref	Expression
1		df-suc	$⊢ suc A = A \cup \{A\}$
2		relsdom	$⊢ Rel ≺$
3	2	brrelex2i	$⊢ 1_{𝑜} ≺ A \to A \in V$
4		1on	$⊢ 1_{𝑜} \in On$
5		xpsneng	$⊢ (A \in V \land 1_{𝑜} \in On) \to (A \times \{1_{𝑜}\}) \approx A$
6	3 4 5	sylancl	$⊢ 1_{𝑜} ≺ A \to (A \times \{1_{𝑜}\}) \approx A$
7	6	ensymd	$⊢ 1_{𝑜} ≺ A \to A \approx (A \times \{1_{𝑜}\})$
8		endom	$⊢ A \approx (A \times \{1_{𝑜}\}) \to A ≼ (A \times \{1_{𝑜}\})$
9	7 8	syl	$⊢ 1_{𝑜} ≺ A \to A ≼ (A \times \{1_{𝑜}\})$
10		ensn1g	$⊢ A \in V \to \{A\} \approx 1_{𝑜}$
11	3 10	syl	$⊢ 1_{𝑜} ≺ A \to \{A\} \approx 1_{𝑜}$
12		ensdomtr	$⊢ (\{A\} \approx 1_{𝑜} \land 1_{𝑜} ≺ A) \to \{A\} ≺ A$
13	11 12	mpancom	$⊢ 1_{𝑜} ≺ A \to \{A\} ≺ A$
14		0ex	$⊢ \emptyset \in V$
15		xpsneng	$⊢ (A \in V \land \emptyset \in V) \to (A \times \{\emptyset\}) \approx A$
16	3 14 15	sylancl	$⊢ 1_{𝑜} ≺ A \to (A \times \{\emptyset\}) \approx A$
17	16	ensymd	$⊢ 1_{𝑜} ≺ A \to A \approx (A \times \{\emptyset\})$
18		sdomentr	$⊢ (\{A\} ≺ A \land A \approx (A \times \{\emptyset\})) \to \{A\} ≺ (A \times \{\emptyset\})$
19	13 17 18	syl2anc	$⊢ 1_{𝑜} ≺ A \to \{A\} ≺ (A \times \{\emptyset\})$
20		sdomdom	$⊢ \{A\} ≺ (A \times \{\emptyset\}) \to \{A\} ≼ (A \times \{\emptyset\})$
21	19 20	syl	$⊢ 1_{𝑜} ≺ A \to \{A\} ≼ (A \times \{\emptyset\})$
22		1n0	$⊢ 1_{𝑜} \neq \emptyset$
23		xpsndisj	$⊢ 1_{𝑜} \neq \emptyset \to (A \times \{1_{𝑜}\}) \cap (A \times \{\emptyset\}) = \emptyset$
24	22 23	mp1i	$⊢ 1_{𝑜} ≺ A \to (A \times \{1_{𝑜}\}) \cap (A \times \{\emptyset\}) = \emptyset$
25		undom	$⊢ ((A ≼ (A \times \{1_{𝑜}\}) \land \{A\} ≼ (A \times \{\emptyset\})) \land (A \times \{1_{𝑜}\}) \cap (A \times \{\emptyset\}) = \emptyset) \to (A \cup \{A\}) ≼ ((A \times \{1_{𝑜}\}) \cup (A \times \{\emptyset\}))$
26	9 21 24 25	syl21anc	$⊢ 1_{𝑜} ≺ A \to (A \cup \{A\}) ≼ ((A \times \{1_{𝑜}\}) \cup (A \times \{\emptyset\}))$
27		sdomentr	$⊢ (1_{𝑜} ≺ A \land A \approx (A \times \{1_{𝑜}\})) \to 1_{𝑜} ≺ (A \times \{1_{𝑜}\})$
28	7 27	mpdan	$⊢ 1_{𝑜} ≺ A \to 1_{𝑜} ≺ (A \times \{1_{𝑜}\})$
29		sdomentr	$⊢ (1_{𝑜} ≺ A \land A \approx (A \times \{\emptyset\})) \to 1_{𝑜} ≺ (A \times \{\emptyset\})$
30	17 29	mpdan	$⊢ 1_{𝑜} ≺ A \to 1_{𝑜} ≺ (A \times \{\emptyset\})$
31		unxpdom	$⊢ (1_{𝑜} ≺ (A \times \{1_{𝑜}\}) \land 1_{𝑜} ≺ (A \times \{\emptyset\})) \to ((A \times \{1_{𝑜}\}) \cup (A \times \{\emptyset\})) ≼ ((A \times \{1_{𝑜}\}) \times (A \times \{\emptyset\}))$
32	28 30 31	syl2anc	$⊢ 1_{𝑜} ≺ A \to ((A \times \{1_{𝑜}\}) \cup (A \times \{\emptyset\})) ≼ ((A \times \{1_{𝑜}\}) \times (A \times \{\emptyset\}))$
33		domtr	$⊢ ((A \cup \{A\}) ≼ ((A \times \{1_{𝑜}\}) \cup (A \times \{\emptyset\})) \land ((A \times \{1_{𝑜}\}) \cup (A \times \{\emptyset\})) ≼ ((A \times \{1_{𝑜}\}) \times (A \times \{\emptyset\}))) \to (A \cup \{A\}) ≼ ((A \times \{1_{𝑜}\}) \times (A \times \{\emptyset\}))$
34	26 32 33	syl2anc	$⊢ 1_{𝑜} ≺ A \to (A \cup \{A\}) ≼ ((A \times \{1_{𝑜}\}) \times (A \times \{\emptyset\}))$
35		xpen	$⊢ ((A \times \{1_{𝑜}\}) \approx A \land (A \times \{\emptyset\}) \approx A) \to ((A \times \{1_{𝑜}\}) \times (A \times \{\emptyset\})) \approx (A \times A)$
36	6 16 35	syl2anc	$⊢ 1_{𝑜} ≺ A \to ((A \times \{1_{𝑜}\}) \times (A \times \{\emptyset\})) \approx (A \times A)$
37		domentr	$⊢ ((A \cup \{A\}) ≼ ((A \times \{1_{𝑜}\}) \times (A \times \{\emptyset\})) \land ((A \times \{1_{𝑜}\}) \times (A \times \{\emptyset\})) \approx (A \times A)) \to (A \cup \{A\}) ≼ (A \times A)$
38	34 36 37	syl2anc	$⊢ 1_{𝑜} ≺ A \to (A \cup \{A\}) ≼ (A \times A)$
39	1 38	eqbrtrid	$⊢ 1_{𝑜} ≺ A \to suc A ≼ (A \times A)$

Metamath Proof Explorer

Theorem sucxpdom

Proof