Metamath Proof Explorer

Theorem disjlem18

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

		Ref	Expression
	Assertion	disjlem18	$⊢ (A \in V \land B \in W) \to (Disj R \to ((x \in dom R \land A \in [x] R) \to (B \in [x] R \leftrightarrow A ≀ R B)))$

Proof

Step	Hyp	Ref	Expression
1		rspe	$⊢ (x \in dom R \land (A \in [x] R \land B \in [x] R)) \to \exists x \in dom R (A \in [x] R \land B \in [x] R)$
2	1	expr	$⊢ (x \in dom R \land A \in [x] R) \to (B \in [x] R \to \exists x \in dom R (A \in [x] R \land B \in [x] R))$
3	2	adantl	$⊢ (((A \in V \land B \in W) \land Disj R) \land (x \in dom R \land A \in [x] R)) \to (B \in [x] R \to \exists x \in dom R (A \in [x] R \land B \in [x] R))$
4		relbrcoss	$⊢ (A \in V \land B \in W) \to (Rel R \to (A ≀ R B \leftrightarrow \exists x \in dom R (A \in [x] R \land B \in [x] R)))$
5		disjrel	$⊢ Disj R \to Rel R$
6	4 5	impel	$⊢ ((A \in V \land B \in W) \land Disj R) \to (A ≀ R B \leftrightarrow \exists x \in dom R (A \in [x] R \land B \in [x] R))$
7	6	adantr	$⊢ (((A \in V \land B \in W) \land Disj R) \land (x \in dom R \land A \in [x] R)) \to (A ≀ R B \leftrightarrow \exists x \in dom R (A \in [x] R \land B \in [x] R))$
8	3 7	sylibrd	$⊢ (((A \in V \land B \in W) \land Disj R) \land (x \in dom R \land A \in [x] R)) \to (B \in [x] R \to A ≀ R B)$
9	8	ex	$⊢ ((A \in V \land B \in W) \land Disj R) \to ((x \in dom R \land A \in [x] R) \to (B \in [x] R \to A ≀ R B))$
10		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))$
11	10	adantl	$⊢ ((A \in V \land B \in W) \land 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))$
12		relbrcoss	$⊢ (A \in V \land B \in W) \to (Rel R \to (A ≀ R B \leftrightarrow \exists y \in dom R (A \in [y] R \land B \in [y] R)))$
13	12 5	impel	$⊢ ((A \in V \land B \in W) \land Disj R) \to (A ≀ R B \leftrightarrow \exists y \in dom R (A \in [y] R \land B \in [y] R))$
14	13	imbi1d	$⊢ ((A \in V \land B \in W) \land Disj R) \to ((A ≀ R B \to B \in [x] R) \leftrightarrow (\exists y \in dom R (A \in [y] R \land B \in [y] R) \to B \in [x] R))$
15	11 14	sylibrd	$⊢ ((A \in V \land B \in W) \land Disj R) \to ((x \in dom R \land A \in [x] R) \to (A ≀ R B \to B \in [x] R))$
16	9 15	impbidd	$⊢ ((A \in V \land B \in W) \land Disj R) \to ((x \in dom R \land A \in [x] R) \to (B \in [x] R \leftrightarrow A ≀ R B))$
17	16	ex	$⊢ (A \in V \land B \in W) \to (Disj R \to ((x \in dom R \land A \in [x] R) \to (B \in [x] R \leftrightarrow A ≀ R B)))$