dfdm5

Description: Definition of domain in terms of 1st and image. (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

		Ref	Expression
	Assertion	dfdm5	$⊢ dom A = ({1^{st} ↾}_{(V \times V)}) [A]$

Proof

Step	Hyp	Ref	Expression
1		excom	$⊢ \exists y \exists p \exists z (p = ⟨z, y⟩ \land (p 1^{st} x \land p \in A)) \leftrightarrow \exists p \exists y \exists z (p = ⟨z, y⟩ \land (p 1^{st} x \land p \in A))$
2		opex	$⊢ ⟨z, y⟩ \in V$
3		breq1	$⊢ p = ⟨z, y⟩ \to (p 1^{st} x \leftrightarrow ⟨z, y⟩ 1^{st} x)$
4		eleq1	$⊢ p = ⟨z, y⟩ \to (p \in A \leftrightarrow ⟨z, y⟩ \in A)$
5	3 4	anbi12d	$⊢ p = ⟨z, y⟩ \to ((p 1^{st} x \land p \in A) \leftrightarrow (⟨z, y⟩ 1^{st} x \land ⟨z, y⟩ \in A))$
6		vex	$⊢ z \in V$
7		vex	$⊢ y \in V$
8	6 7	br1steq	$⊢ ⟨z, y⟩ 1^{st} x \leftrightarrow x = z$
9		equcom	$⊢ x = z \leftrightarrow z = x$
10	8 9	bitri	$⊢ ⟨z, y⟩ 1^{st} x \leftrightarrow z = x$
11	10	anbi1i	$⊢ (⟨z, y⟩ 1^{st} x \land ⟨z, y⟩ \in A) \leftrightarrow (z = x \land ⟨z, y⟩ \in A)$
12	5 11	bitrdi	$⊢ p = ⟨z, y⟩ \to ((p 1^{st} x \land p \in A) \leftrightarrow (z = x \land ⟨z, y⟩ \in A))$
13	2 12	ceqsexv	$⊢ \exists p (p = ⟨z, y⟩ \land (p 1^{st} x \land p \in A)) \leftrightarrow (z = x \land ⟨z, y⟩ \in A)$
14	13	exbii	$⊢ \exists z \exists p (p = ⟨z, y⟩ \land (p 1^{st} x \land p \in A)) \leftrightarrow \exists z (z = x \land ⟨z, y⟩ \in A)$
15		excom	$⊢ \exists z \exists p (p = ⟨z, y⟩ \land (p 1^{st} x \land p \in A)) \leftrightarrow \exists p \exists z (p = ⟨z, y⟩ \land (p 1^{st} x \land p \in A))$
16		vex	$⊢ x \in V$
17		opeq1	$⊢ z = x \to ⟨z, y⟩ = ⟨x, y⟩$
18	17	eleq1d	$⊢ z = x \to (⟨z, y⟩ \in A \leftrightarrow ⟨x, y⟩ \in A)$
19	16 18	ceqsexv	$⊢ \exists z (z = x \land ⟨z, y⟩ \in A) \leftrightarrow ⟨x, y⟩ \in A$
20	14 15 19	3bitr3ri	$⊢ ⟨x, y⟩ \in A \leftrightarrow \exists p \exists z (p = ⟨z, y⟩ \land (p 1^{st} x \land p \in A))$
21	20	exbii	$⊢ \exists y ⟨x, y⟩ \in A \leftrightarrow \exists y \exists p \exists z (p = ⟨z, y⟩ \land (p 1^{st} x \land p \in A))$
22		ancom	$⊢ (p \in A \land p ({1^{st} ↾}_{(V \times V)}) x) \leftrightarrow (p ({1^{st} ↾}_{(V \times V)}) x \land p \in A)$
23		anass	$⊢ ((\exists y \exists z p = ⟨z, y⟩ \land p 1^{st} x) \land p \in A) \leftrightarrow (\exists y \exists z p = ⟨z, y⟩ \land (p 1^{st} x \land p \in A))$
24	16	brresi	$⊢ p ({1^{st} ↾}_{(V \times V)}) x \leftrightarrow (p \in (V \times V) \land p 1^{st} x)$
25		elvv	$⊢ p \in (V \times V) \leftrightarrow \exists z \exists y p = ⟨z, y⟩$
26		excom	$⊢ \exists z \exists y p = ⟨z, y⟩ \leftrightarrow \exists y \exists z p = ⟨z, y⟩$
27	25 26	bitri	$⊢ p \in (V \times V) \leftrightarrow \exists y \exists z p = ⟨z, y⟩$
28	27	anbi1i	$⊢ (p \in (V \times V) \land p 1^{st} x) \leftrightarrow (\exists y \exists z p = ⟨z, y⟩ \land p 1^{st} x)$
29	24 28	bitri	$⊢ p ({1^{st} ↾}_{(V \times V)}) x \leftrightarrow (\exists y \exists z p = ⟨z, y⟩ \land p 1^{st} x)$
30	29	anbi1i	$⊢ (p ({1^{st} ↾}_{(V \times V)}) x \land p \in A) \leftrightarrow ((\exists y \exists z p = ⟨z, y⟩ \land p 1^{st} x) \land p \in A)$
31		19.41vv	$⊢ \exists y \exists z (p = ⟨z, y⟩ \land (p 1^{st} x \land p \in A)) \leftrightarrow (\exists y \exists z p = ⟨z, y⟩ \land (p 1^{st} x \land p \in A))$
32	23 30 31	3bitr4i	$⊢ (p ({1^{st} ↾}_{(V \times V)}) x \land p \in A) \leftrightarrow \exists y \exists z (p = ⟨z, y⟩ \land (p 1^{st} x \land p \in A))$
33	22 32	bitri	$⊢ (p \in A \land p ({1^{st} ↾}_{(V \times V)}) x) \leftrightarrow \exists y \exists z (p = ⟨z, y⟩ \land (p 1^{st} x \land p \in A))$
34	33	exbii	$⊢ \exists p (p \in A \land p ({1^{st} ↾}_{(V \times V)}) x) \leftrightarrow \exists p \exists y \exists z (p = ⟨z, y⟩ \land (p 1^{st} x \land p \in A))$
35	1 21 34	3bitr4i	$⊢ \exists y ⟨x, y⟩ \in A \leftrightarrow \exists p (p \in A \land p ({1^{st} ↾}_{(V \times V)}) x)$
36	16	eldm2	$⊢ x \in dom A \leftrightarrow \exists y ⟨x, y⟩ \in A$
37	16	elima2	$⊢ x \in ({1^{st} ↾}_{(V \times V)}) [A] \leftrightarrow \exists p (p \in A \land p ({1^{st} ↾}_{(V \times V)}) x)$
38	35 36 37	3bitr4i	$⊢ x \in dom A \leftrightarrow x \in ({1^{st} ↾}_{(V \times V)}) [A]$
39	38	eqriv	$⊢ dom A = ({1^{st} ↾}_{(V \times V)}) [A]$

Metamath Proof Explorer

Theorem dfdm5

Proof