canthp1lem1

		Ref	Expression
	Assertion	canthp1lem1	$⊢ 1_{𝑜} ≺ A \to (A ⊔︀ 2_{𝑜}) ≼ 𝒫 A$

Proof

Step	Hyp	Ref	Expression
1		1sdom2	$⊢ 1_{𝑜} ≺ 2_{𝑜}$
2		djuxpdom	$⊢ (1_{𝑜} ≺ A \land 1_{𝑜} ≺ 2_{𝑜}) \to (A ⊔︀ 2_{𝑜}) ≼ (A \times 2_{𝑜})$
3	1 2	mpan2	$⊢ 1_{𝑜} ≺ A \to (A ⊔︀ 2_{𝑜}) ≼ (A \times 2_{𝑜})$
4		sdom0	$⊢ \neg 1_{𝑜} ≺ \emptyset$
5		breq2	$⊢ A = \emptyset \to (1_{𝑜} ≺ A \leftrightarrow 1_{𝑜} ≺ \emptyset)$
6	4 5	mtbiri	$⊢ A = \emptyset \to \neg 1_{𝑜} ≺ A$
7	6	con2i	$⊢ 1_{𝑜} ≺ A \to \neg A = \emptyset$
8		neq0	$⊢ \neg A = \emptyset \leftrightarrow \exists x x \in A$
9	7 8	sylib	$⊢ 1_{𝑜} ≺ A \to \exists x x \in A$
10		relsdom	$⊢ Rel ≺$
11	10	brrelex2i	$⊢ 1_{𝑜} ≺ A \to A \in V$
12	11	adantr	$⊢ (1_{𝑜} ≺ A \land x \in A) \to A \in V$
13		enrefg	$⊢ A \in V \to A \approx A$
14	12 13	syl	$⊢ (1_{𝑜} ≺ A \land x \in A) \to A \approx A$
15		df2o2	$⊢ 2_{𝑜} = \{\emptyset, \{\emptyset\}\}$
16		pwpw0	$⊢ 𝒫 \{\emptyset\} = \{\emptyset, \{\emptyset\}\}$
17	15 16	eqtr4i	$⊢ 2_{𝑜} = 𝒫 \{\emptyset\}$
18		0ex	$⊢ \emptyset \in V$
19		vex	$⊢ x \in V$
20		en2sn	$⊢ (\emptyset \in V \land x \in V) \to \{\emptyset\} \approx \{x\}$
21	18 19 20	mp2an	$⊢ \{\emptyset\} \approx \{x\}$
22		pwen	$⊢ \{\emptyset\} \approx \{x\} \to 𝒫 \{\emptyset\} \approx 𝒫 \{x\}$
23	21 22	ax-mp	$⊢ 𝒫 \{\emptyset\} \approx 𝒫 \{x\}$
24	17 23	eqbrtri	$⊢ 2_{𝑜} \approx 𝒫 \{x\}$
25		xpen	$⊢ (A \approx A \land 2_{𝑜} \approx 𝒫 \{x\}) \to (A \times 2_{𝑜}) \approx (A \times 𝒫 \{x\})$
26	14 24 25	sylancl	$⊢ (1_{𝑜} ≺ A \land x \in A) \to (A \times 2_{𝑜}) \approx (A \times 𝒫 \{x\})$
27		snex	$⊢ \{x\} \in V$
28	27	pwex	$⊢ 𝒫 \{x\} \in V$
29		uncom	$⊢ (A ∖ \{x\}) \cup \{x\} = \{x\} \cup (A ∖ \{x\})$
30		simpr	$⊢ (1_{𝑜} ≺ A \land x \in A) \to x \in A$
31	30	snssd	$⊢ (1_{𝑜} ≺ A \land x \in A) \to \{x\} \subseteq A$
32		undif	$⊢ \{x\} \subseteq A \leftrightarrow \{x\} \cup (A ∖ \{x\}) = A$
33	31 32	sylib	$⊢ (1_{𝑜} ≺ A \land x \in A) \to \{x\} \cup (A ∖ \{x\}) = A$
34	29 33	syl5eq	$⊢ (1_{𝑜} ≺ A \land x \in A) \to (A ∖ \{x\}) \cup \{x\} = A$
35		difexg	$⊢ A \in V \to A ∖ \{x\} \in V$
36	12 35	syl	$⊢ (1_{𝑜} ≺ A \land x \in A) \to A ∖ \{x\} \in V$
37		canth2g	$⊢ A ∖ \{x\} \in V \to (A ∖ \{x\}) ≺ 𝒫 (A ∖ \{x\})$
38		domunsn	$⊢ (A ∖ \{x\}) ≺ 𝒫 (A ∖ \{x\}) \to ((A ∖ \{x\}) \cup \{x\}) ≼ 𝒫 (A ∖ \{x\})$
39	36 37 38	3syl	$⊢ (1_{𝑜} ≺ A \land x \in A) \to ((A ∖ \{x\}) \cup \{x\}) ≼ 𝒫 (A ∖ \{x\})$
40	34 39	eqbrtrrd	$⊢ (1_{𝑜} ≺ A \land x \in A) \to A ≼ 𝒫 (A ∖ \{x\})$
41		xpdom1g	$⊢ (𝒫 \{x\} \in V \land A ≼ 𝒫 (A ∖ \{x\})) \to (A \times 𝒫 \{x\}) ≼ (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\})$
42	28 40 41	sylancr	$⊢ (1_{𝑜} ≺ A \land x \in A) \to (A \times 𝒫 \{x\}) ≼ (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\})$
43		endomtr	$⊢ ((A \times 2_{𝑜}) \approx (A \times 𝒫 \{x\}) \land (A \times 𝒫 \{x\}) ≼ (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\})) \to (A \times 2_{𝑜}) ≼ (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\})$
44	26 42 43	syl2anc	$⊢ (1_{𝑜} ≺ A \land x \in A) \to (A \times 2_{𝑜}) ≼ (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\})$
45		pwdjuen	$⊢ (A ∖ \{x\} \in V \land \{x\} \in V) \to 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\}) \approx (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\})$
46	36 27 45	sylancl	$⊢ (1_{𝑜} ≺ A \land x \in A) \to 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\}) \approx (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\})$
47	46	ensymd	$⊢ (1_{𝑜} ≺ A \land x \in A) \to (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\}) \approx 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\})$
48		domentr	$⊢ ((A \times 2_{𝑜}) ≼ (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\}) \land (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\}) \approx 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\})) \to (A \times 2_{𝑜}) ≼ 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\})$
49	44 47 48	syl2anc	$⊢ (1_{𝑜} ≺ A \land x \in A) \to (A \times 2_{𝑜}) ≼ 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\})$
50	27	a1i	$⊢ (1_{𝑜} ≺ A \land x \in A) \to \{x\} \in V$
51		incom	$⊢ (A ∖ \{x\}) \cap \{x\} = \{x\} \cap (A ∖ \{x\})$
52		disjdif	$⊢ \{x\} \cap (A ∖ \{x\}) = \emptyset$
53	51 52	eqtri	$⊢ (A ∖ \{x\}) \cap \{x\} = \emptyset$
54	53	a1i	$⊢ (1_{𝑜} ≺ A \land x \in A) \to (A ∖ \{x\}) \cap \{x\} = \emptyset$
55		endjudisj	$⊢ (A ∖ \{x\} \in V \land \{x\} \in V \land (A ∖ \{x\}) \cap \{x\} = \emptyset) \to ((A ∖ \{x\}) ⊔︀ \{x\}) \approx ((A ∖ \{x\}) \cup \{x\})$
56	36 50 54 55	syl3anc	$⊢ (1_{𝑜} ≺ A \land x \in A) \to ((A ∖ \{x\}) ⊔︀ \{x\}) \approx ((A ∖ \{x\}) \cup \{x\})$
57	56 34	breqtrd	$⊢ (1_{𝑜} ≺ A \land x \in A) \to ((A ∖ \{x\}) ⊔︀ \{x\}) \approx A$
58		pwen	$⊢ ((A ∖ \{x\}) ⊔︀ \{x\}) \approx A \to 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\}) \approx 𝒫 A$
59	57 58	syl	$⊢ (1_{𝑜} ≺ A \land x \in A) \to 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\}) \approx 𝒫 A$
60		domentr	$⊢ ((A \times 2_{𝑜}) ≼ 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\}) \land 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\}) \approx 𝒫 A) \to (A \times 2_{𝑜}) ≼ 𝒫 A$
61	49 59 60	syl2anc	$⊢ (1_{𝑜} ≺ A \land x \in A) \to (A \times 2_{𝑜}) ≼ 𝒫 A$
62	9 61	exlimddv	$⊢ 1_{𝑜} ≺ A \to (A \times 2_{𝑜}) ≼ 𝒫 A$
63		domtr	$⊢ ((A ⊔︀ 2_{𝑜}) ≼ (A \times 2_{𝑜}) \land (A \times 2_{𝑜}) ≼ 𝒫 A) \to (A ⊔︀ 2_{𝑜}) ≼ 𝒫 A$
64	3 62 63	syl2anc	$⊢ 1_{𝑜} ≺ A \to (A ⊔︀ 2_{𝑜}) ≼ 𝒫 A$

Metamath Proof Explorer

Theorem canthp1lem1

Proof