disjen

Description: A stronger form of pwuninel . We can use pwuninel , 2pwuninel to create one or two sets disjoint from a given set A , but here we show that in fact such constructions exist for arbitrarily large disjoint extensions, which is to say that for any set B we can construct a set x that is equinumerous to it and disjoint from A . (Contributed by Mario Carneiro, 7-Feb-2015)

		Ref	Expression
	Assertion	disjen	$⊢ (A \in V \land B \in W) \to (A \cap (B \times \{𝒫 ⋃ ran A\}) = \emptyset \land (B \times \{𝒫 ⋃ ran A\}) \approx B)$

Proof

Step	Hyp	Ref	Expression
1		1st2nd2	$⊢ x \in (B \times \{𝒫 ⋃ ran A\}) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
2	1	ad2antll	$⊢ ((A \in V \land B \in W) \land (x \in A \land x \in (B \times \{𝒫 ⋃ ran A\}))) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
3		simprl	$⊢ ((A \in V \land B \in W) \land (x \in A \land x \in (B \times \{𝒫 ⋃ ran A\}))) \to x \in A$
4	2 3	eqeltrrd	$⊢ ((A \in V \land B \in W) \land (x \in A \land x \in (B \times \{𝒫 ⋃ ran A\}))) \to ⟨1^{st} (x), 2^{nd} (x)⟩ \in A$
5		fvex	$⊢ 1^{st} (x) \in V$
6		fvex	$⊢ 2^{nd} (x) \in V$
7	5 6	opelrn	$⊢ ⟨1^{st} (x), 2^{nd} (x)⟩ \in A \to 2^{nd} (x) \in ran A$
8	4 7	syl	$⊢ ((A \in V \land B \in W) \land (x \in A \land x \in (B \times \{𝒫 ⋃ ran A\}))) \to 2^{nd} (x) \in ran A$
9		pwuninel	$⊢ \neg 𝒫 ⋃ ran A \in ran A$
10		xp2nd	$⊢ x \in (B \times \{𝒫 ⋃ ran A\}) \to 2^{nd} (x) \in \{𝒫 ⋃ ran A\}$
11	10	ad2antll	$⊢ ((A \in V \land B \in W) \land (x \in A \land x \in (B \times \{𝒫 ⋃ ran A\}))) \to 2^{nd} (x) \in \{𝒫 ⋃ ran A\}$
12		elsni	$⊢ 2^{nd} (x) \in \{𝒫 ⋃ ran A\} \to 2^{nd} (x) = 𝒫 ⋃ ran A$
13	11 12	syl	$⊢ ((A \in V \land B \in W) \land (x \in A \land x \in (B \times \{𝒫 ⋃ ran A\}))) \to 2^{nd} (x) = 𝒫 ⋃ ran A$
14	13	eleq1d	$⊢ ((A \in V \land B \in W) \land (x \in A \land x \in (B \times \{𝒫 ⋃ ran A\}))) \to (2^{nd} (x) \in ran A \leftrightarrow 𝒫 ⋃ ran A \in ran A)$
15	9 14	mtbiri	$⊢ ((A \in V \land B \in W) \land (x \in A \land x \in (B \times \{𝒫 ⋃ ran A\}))) \to \neg 2^{nd} (x) \in ran A$
16	8 15	pm2.65da	$⊢ (A \in V \land B \in W) \to \neg (x \in A \land x \in (B \times \{𝒫 ⋃ ran A\}))$
17		elin	$⊢ x \in (A \cap (B \times \{𝒫 ⋃ ran A\})) \leftrightarrow (x \in A \land x \in (B \times \{𝒫 ⋃ ran A\}))$
18	16 17	sylnibr	$⊢ (A \in V \land B \in W) \to \neg x \in (A \cap (B \times \{𝒫 ⋃ ran A\}))$
19	18	eq0rdv	$⊢ (A \in V \land B \in W) \to A \cap (B \times \{𝒫 ⋃ ran A\}) = \emptyset$
20		simpr	$⊢ (A \in V \land B \in W) \to B \in W$
21		rnexg	$⊢ A \in V \to ran A \in V$
22	21	adantr	$⊢ (A \in V \land B \in W) \to ran A \in V$
23		uniexg	$⊢ ran A \in V \to ⋃ ran A \in V$
24		pwexg	$⊢ ⋃ ran A \in V \to 𝒫 ⋃ ran A \in V$
25	22 23 24	3syl	$⊢ (A \in V \land B \in W) \to 𝒫 ⋃ ran A \in V$
26		xpsneng	$⊢ (B \in W \land 𝒫 ⋃ ran A \in V) \to (B \times \{𝒫 ⋃ ran A\}) \approx B$
27	20 25 26	syl2anc	$⊢ (A \in V \land B \in W) \to (B \times \{𝒫 ⋃ ran A\}) \approx B$
28	19 27	jca	$⊢ (A \in V \land B \in W) \to (A \cap (B \times \{𝒫 ⋃ ran A\}) = \emptyset \land (B \times \{𝒫 ⋃ ran A\}) \approx B)$

Metamath Proof Explorer

Theorem disjen

Proof