Metamath Proof Explorer

Theorem disjlem17

Description: Lemma for disjdmqseq , partim2 and petlem via disjlem18 , (general version of the former prtlem17 ). (Contributed by Peter Mazsa, 10-Sep-2021)

		Ref	Expression
	Assertion	disjlem17	$⊢ Disj R \to ((x \in dom R \land A \in [x] R) \to (\exists y \in dom R (A \in [y] R \land B \in [y] R) \to B \in [x] R))$

Proof

Step	Hyp	Ref	Expression
1		df-rex	$⊢ \exists y \in dom R (A \in [y] R \land B \in [y] R) \leftrightarrow \exists y (y \in dom R \land (A \in [y] R \land B \in [y] R))$
2		an32	$⊢ ((x \in dom R \land y \in dom R) \land A \in [x] R) \leftrightarrow ((x \in dom R \land A \in [x] R) \land y \in dom R)$
3		disjlem14	$⊢ Disj R \to ((x \in dom R \land y \in dom R) \to ((A \in [x] R \land A \in [y] R) \to [x] R = [y] R))$
4		eleq2	$⊢ [x] R = [y] R \to (B \in [x] R \leftrightarrow B \in [y] R)$
5	4	biimprd	$⊢ [x] R = [y] R \to (B \in [y] R \to B \in [x] R)$
6	3 5	syl8	$⊢ Disj R \to ((x \in dom R \land y \in dom R) \to ((A \in [x] R \land A \in [y] R) \to (B \in [y] R \to B \in [x] R)))$
7	6	exp4a	$⊢ Disj R \to ((x \in dom R \land y \in dom R) \to (A \in [x] R \to (A \in [y] R \to (B \in [y] R \to B \in [x] R))))$
8	7	impd	$⊢ Disj R \to (((x \in dom R \land y \in dom R) \land A \in [x] R) \to (A \in [y] R \to (B \in [y] R \to B \in [x] R)))$
9	2 8	biimtrrid	$⊢ Disj R \to (((x \in dom R \land A \in [x] R) \land y \in dom R) \to (A \in [y] R \to (B \in [y] R \to B \in [x] R)))$
10	9	expd	$⊢ Disj R \to ((x \in dom R \land A \in [x] R) \to (y \in dom R \to (A \in [y] R \to (B \in [y] R \to B \in [x] R))))$
11	10	imp5a	$⊢ Disj R \to ((x \in dom R \land A \in [x] R) \to (y \in dom R \to ((A \in [y] R \land B \in [y] R) \to B \in [x] R)))$
12	11	imp4b	$⊢ (Disj R \land (x \in dom R \land A \in [x] R)) \to ((y \in dom R \land (A \in [y] R \land B \in [y] R)) \to B \in [x] R)$
13	12	exlimdv	$⊢ (Disj R \land (x \in dom R \land A \in [x] R)) \to (\exists y (y \in dom R \land (A \in [y] R \land B \in [y] R)) \to B \in [x] R)$
14	1 13	biimtrid	$⊢ (Disj R \land (x \in dom R \land A \in [x] R)) \to (\exists y \in dom R (A \in [y] R \land B \in [y] R) \to B \in [x] R)$
15	14	ex	$⊢ Disj R \to ((x \in dom R \land A \in [x] R) \to (\exists y \in dom R (A \in [y] R \land B \in [y] R) \to B \in [x] R))$