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	12	difexd	$⊢ (1_{𝑜} ≺ A \land x \in A) \to A ∖ \{x\} \in V$
36		canth2g	$⊢ A ∖ \{x\} \in V \to (A ∖ \{x\}) ≺ 𝒫 (A ∖ \{x\})$
37		domunsn	$⊢ (A ∖ \{x\}) ≺ 𝒫 (A ∖ \{x\}) \to ((A ∖ \{x\}) \cup \{x\}) ≼ 𝒫 (A ∖ \{x\})$
38	35 36 37	3syl	$⊢ (1_{𝑜} ≺ A \land x \in A) \to ((A ∖ \{x\}) \cup \{x\}) ≼ 𝒫 (A ∖ \{x\})$
39	34 38	eqbrtrrd	$⊢ (1_{𝑜} ≺ A \land x \in A) \to A ≼ 𝒫 (A ∖ \{x\})$
40		xpdom1g	$⊢ (𝒫 \{x\} \in V \land A ≼ 𝒫 (A ∖ \{x\})) \to (A \times 𝒫 \{x\}) ≼ (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\})$
41	28 39 40	sylancr	$⊢ (1_{𝑜} ≺ A \land x \in A) \to (A \times 𝒫 \{x\}) ≼ (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\})$
42		endomtr	$⊢ ((A \times 2_{𝑜}) \approx (A \times 𝒫 \{x\}) \land (A \times 𝒫 \{x\}) ≼ (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\})) \to (A \times 2_{𝑜}) ≼ (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\})$
43	26 41 42	syl2anc	$⊢ (1_{𝑜} ≺ A \land x \in A) \to (A \times 2_{𝑜}) ≼ (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\})$
44		pwdjuen	$⊢ (A ∖ \{x\} \in V \land \{x\} \in V) \to 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\}) \approx (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\})$
45	35 27 44	sylancl	$⊢ (1_{𝑜} ≺ A \land x \in A) \to 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\}) \approx (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\})$
46	45	ensymd	$⊢ (1_{𝑜} ≺ A \land x \in A) \to (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\}) \approx 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\})$
47		domentr	$⊢ ((A \times 2_{𝑜}) ≼ (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\}) \land (𝒫 (A ∖ \{x\}) \times 𝒫 \{x\}) \approx 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\})) \to (A \times 2_{𝑜}) ≼ 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\})$
48	43 46 47	syl2anc	$⊢ (1_{𝑜} ≺ A \land x \in A) \to (A \times 2_{𝑜}) ≼ 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\})$
49	27	a1i	$⊢ (1_{𝑜} ≺ A \land x \in A) \to \{x\} \in V$
50		disjdifr	$⊢ (A ∖ \{x\}) \cap \{x\} = \emptyset$
51	50	a1i	$⊢ (1_{𝑜} ≺ A \land x \in A) \to (A ∖ \{x\}) \cap \{x\} = \emptyset$
52		endjudisj	$⊢ (A ∖ \{x\} \in V \land \{x\} \in V \land (A ∖ \{x\}) \cap \{x\} = \emptyset) \to ((A ∖ \{x\}) ⊔︀ \{x\}) \approx ((A ∖ \{x\}) \cup \{x\})$
53	35 49 51 52	syl3anc	$⊢ (1_{𝑜} ≺ A \land x \in A) \to ((A ∖ \{x\}) ⊔︀ \{x\}) \approx ((A ∖ \{x\}) \cup \{x\})$
54	53 34	breqtrd	$⊢ (1_{𝑜} ≺ A \land x \in A) \to ((A ∖ \{x\}) ⊔︀ \{x\}) \approx A$
55		pwen	$⊢ ((A ∖ \{x\}) ⊔︀ \{x\}) \approx A \to 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\}) \approx 𝒫 A$
56	54 55	syl	$⊢ (1_{𝑜} ≺ A \land x \in A) \to 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\}) \approx 𝒫 A$
57		domentr	$⊢ ((A \times 2_{𝑜}) ≼ 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\}) \land 𝒫 ((A ∖ \{x\}) ⊔︀ \{x\}) \approx 𝒫 A) \to (A \times 2_{𝑜}) ≼ 𝒫 A$
58	48 56 57	syl2anc	$⊢ (1_{𝑜} ≺ A \land x \in A) \to (A \times 2_{𝑜}) ≼ 𝒫 A$
59	9 58	exlimddv	$⊢ 1_{𝑜} ≺ A \to (A \times 2_{𝑜}) ≼ 𝒫 A$
60		domtr	$⊢ ((A ⊔︀ 2_{𝑜}) ≼ (A \times 2_{𝑜}) \land (A \times 2_{𝑜}) ≼ 𝒫 A) \to (A ⊔︀ 2_{𝑜}) ≼ 𝒫 A$
61	3 59 60	syl2anc	$⊢ 1_{𝑜} ≺ A \to (A ⊔︀ 2_{𝑜}) ≼ 𝒫 A$

Metamath Proof Explorer

Theorem canthp1lem1

Proof