prtlem16

		Ref	Expression
	Hypothesis	prtlem13.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\}$
	Assertion	prtlem16	$⊢ dom \underset{˙}{\sim} = ⋃ A$

Proof

Step	Hyp	Ref	Expression
1		prtlem13.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\}$
2		vex	$⊢ z \in V$
3	2	eldm	$⊢ z \in dom \underset{˙}{\sim} \leftrightarrow \exists w z \underset{˙}{\sim} w$
4	1	prtlem13	$⊢ z \underset{˙}{\sim} w \leftrightarrow \exists v \in A (z \in v \land w \in v)$
5	4	exbii	$⊢ \exists w z \underset{˙}{\sim} w \leftrightarrow \exists w \exists v \in A (z \in v \land w \in v)$
6		elunii	$⊢ (z \in v \land v \in A) \to z \in ⋃ A$
7	6	ancoms	$⊢ (v \in A \land z \in v) \to z \in ⋃ A$
8	7	adantrr	$⊢ (v \in A \land (z \in v \land w \in v)) \to z \in ⋃ A$
9	8	rexlimiva	$⊢ \exists v \in A (z \in v \land w \in v) \to z \in ⋃ A$
10	9	exlimiv	$⊢ \exists w \exists v \in A (z \in v \land w \in v) \to z \in ⋃ A$
11		eluni2	$⊢ z \in ⋃ A \leftrightarrow \exists v \in A z \in v$
12		elequ1	$⊢ w = z \to (w \in v \leftrightarrow z \in v)$
13	12	anbi2d	$⊢ w = z \to ((z \in v \land w \in v) \leftrightarrow (z \in v \land z \in v))$
14		pm4.24	$⊢ z \in v \leftrightarrow (z \in v \land z \in v)$
15	13 14	bitr4di	$⊢ w = z \to ((z \in v \land w \in v) \leftrightarrow z \in v)$
16	15	rexbidv	$⊢ w = z \to (\exists v \in A (z \in v \land w \in v) \leftrightarrow \exists v \in A z \in v)$
17	2 16	spcev	$⊢ \exists v \in A z \in v \to \exists w \exists v \in A (z \in v \land w \in v)$
18	11 17	sylbi	$⊢ z \in ⋃ A \to \exists w \exists v \in A (z \in v \land w \in v)$
19	10 18	impbii	$⊢ \exists w \exists v \in A (z \in v \land w \in v) \leftrightarrow z \in ⋃ A$
20	3 5 19	3bitri	$⊢ z \in dom \underset{˙}{\sim} \leftrightarrow z \in ⋃ A$
21	20	eqriv	$⊢ dom \underset{˙}{\sim} = ⋃ A$

Metamath Proof Explorer

Theorem prtlem16

Proof