dfrn5

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

		Ref	Expression
	Assertion	dfrn5	$⊢ ran A = ({2^{nd} ↾}_{(V \times V)}) [A]$

Proof

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

Metamath Proof Explorer

Theorem dfrn5

Proof