disjenex

Description: Existence version of disjen . (Contributed by Mario Carneiro, 7-Feb-2015)

		Ref	Expression
	Assertion	disjenex	$⊢ (A \in V \land B \in W) \to \exists x (A \cap x = \emptyset \land x \approx B)$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (A \in V \land B \in W) \to B \in W$
2		snex	$⊢ \{𝒫 ⋃ ran A\} \in V$
3		xpexg	$⊢ (B \in W \land \{𝒫 ⋃ ran A\} \in V) \to B \times \{𝒫 ⋃ ran A\} \in V$
4	1 2 3	sylancl	$⊢ (A \in V \land B \in W) \to B \times \{𝒫 ⋃ ran A\} \in V$
5		disjen	$⊢ (A \in V \land B \in W) \to (A \cap (B \times \{𝒫 ⋃ ran A\}) = \emptyset \land (B \times \{𝒫 ⋃ ran A\}) \approx B)$
6		ineq2	$⊢ x = B \times \{𝒫 ⋃ ran A\} \to A \cap x = A \cap (B \times \{𝒫 ⋃ ran A\})$
7	6	eqeq1d	$⊢ x = B \times \{𝒫 ⋃ ran A\} \to (A \cap x = \emptyset \leftrightarrow A \cap (B \times \{𝒫 ⋃ ran A\}) = \emptyset)$
8		breq1	$⊢ x = B \times \{𝒫 ⋃ ran A\} \to (x \approx B \leftrightarrow (B \times \{𝒫 ⋃ ran A\}) \approx B)$
9	7 8	anbi12d	$⊢ x = B \times \{𝒫 ⋃ ran A\} \to ((A \cap x = \emptyset \land x \approx B) \leftrightarrow (A \cap (B \times \{𝒫 ⋃ ran A\}) = \emptyset \land (B \times \{𝒫 ⋃ ran A\}) \approx B))$
10	4 5 9	spcedv	$⊢ (A \in V \land B \in W) \to \exists x (A \cap x = \emptyset \land x \approx B)$

Metamath Proof Explorer