Theorem 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 𝐴 = ( ( 2nd ↾ ( V × V ) ) “ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		excom	⊢ ( ∃ 𝑦 ∃ 𝑝 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ) ↔ ∃ 𝑝 ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ) )
2		opex	⊢ ⟨ 𝑦 , 𝑧 ⟩ ∈ V
3		breq1	⊢ ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑝 2nd 𝑥 ↔ ⟨ 𝑦 , 𝑧 ⟩ 2nd 𝑥 ) )
4		eleq1	⊢ ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑝 ∈ 𝐴 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ) )
5	3 4	anbi12d	⊢ ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ↔ ( ⟨ 𝑦 , 𝑧 ⟩ 2nd 𝑥 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ) ) )
6		vex	⊢ 𝑦 ∈ V
7		vex	⊢ 𝑧 ∈ V
8	6 7	br2ndeq	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ 2nd 𝑥 ↔ 𝑥 = 𝑧 )
9		equcom	⊢ ( 𝑥 = 𝑧 ↔ 𝑧 = 𝑥 )
10	8 9	bitri	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ 2nd 𝑥 ↔ 𝑧 = 𝑥 )
11	10	anbi1i	⊢ ( ( ⟨ 𝑦 , 𝑧 ⟩ 2nd 𝑥 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ) ↔ ( 𝑧 = 𝑥 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ) )
12	5 11	bitrdi	⊢ ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ↔ ( 𝑧 = 𝑥 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ) ) )
13	2 12	ceqsexv	⊢ ( ∃ 𝑝 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ) ↔ ( 𝑧 = 𝑥 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ) )
14	13	exbii	⊢ ( ∃ 𝑧 ∃ 𝑝 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ) )
15		excom	⊢ ( ∃ 𝑧 ∃ 𝑝 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ) ↔ ∃ 𝑝 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ) )
16		vex	⊢ 𝑥 ∈ V
17		opeq2	⊢ ( 𝑧 = 𝑥 → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑦 , 𝑥 ⟩ )
18	17	eleq1d	⊢ ( 𝑧 = 𝑥 → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐴 ) )
19	16 18	ceqsexv	⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 ) ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐴 )
20	14 15 19	3bitr3ri	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐴 ↔ ∃ 𝑝 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ) )
21	20	exbii	⊢ ( ∃ 𝑦 ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐴 ↔ ∃ 𝑦 ∃ 𝑝 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ) )
22		ancom	⊢ ( ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( 2nd ↾ ( V × V ) ) 𝑥 ) ↔ ( 𝑝 ( 2nd ↾ ( V × V ) ) 𝑥 ∧ 𝑝 ∈ 𝐴 ) )
23		anass	⊢ ( ( ( ∃ 𝑦 ∃ 𝑧 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑝 2nd 𝑥 ) ∧ 𝑝 ∈ 𝐴 ) ↔ ( ∃ 𝑦 ∃ 𝑧 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ) )
24	16	brresi	⊢ ( 𝑝 ( 2nd ↾ ( V × V ) ) 𝑥 ↔ ( 𝑝 ∈ ( V × V ) ∧ 𝑝 2nd 𝑥 ) )
25		elvv	⊢ ( 𝑝 ∈ ( V × V ) ↔ ∃ 𝑦 ∃ 𝑧 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ )
26	25	anbi1i	⊢ ( ( 𝑝 ∈ ( V × V ) ∧ 𝑝 2nd 𝑥 ) ↔ ( ∃ 𝑦 ∃ 𝑧 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑝 2nd 𝑥 ) )
27	24 26	bitri	⊢ ( 𝑝 ( 2nd ↾ ( V × V ) ) 𝑥 ↔ ( ∃ 𝑦 ∃ 𝑧 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑝 2nd 𝑥 ) )
28	27	anbi1i	⊢ ( ( 𝑝 ( 2nd ↾ ( V × V ) ) 𝑥 ∧ 𝑝 ∈ 𝐴 ) ↔ ( ( ∃ 𝑦 ∃ 𝑧 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑝 2nd 𝑥 ) ∧ 𝑝 ∈ 𝐴 ) )
29		19.41vv	⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ) ↔ ( ∃ 𝑦 ∃ 𝑧 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ) )
30	23 28 29	3bitr4i	⊢ ( ( 𝑝 ( 2nd ↾ ( V × V ) ) 𝑥 ∧ 𝑝 ∈ 𝐴 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ) )
31	22 30	bitri	⊢ ( ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( 2nd ↾ ( V × V ) ) 𝑥 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ) )
32	31	exbii	⊢ ( ∃ 𝑝 ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( 2nd ↾ ( V × V ) ) 𝑥 ) ↔ ∃ 𝑝 ∃ 𝑦 ∃ 𝑧 ( 𝑝 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑝 2nd 𝑥 ∧ 𝑝 ∈ 𝐴 ) ) )
33	1 21 32	3bitr4i	⊢ ( ∃ 𝑦 ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐴 ↔ ∃ 𝑝 ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( 2nd ↾ ( V × V ) ) 𝑥 ) )
34	16	elrn2	⊢ ( 𝑥 ∈ ran 𝐴 ↔ ∃ 𝑦 ⟨ 𝑦 , 𝑥 ⟩ ∈ 𝐴 )
35	16	elima2	⊢ ( 𝑥 ∈ ( ( 2nd ↾ ( V × V ) ) “ 𝐴 ) ↔ ∃ 𝑝 ( 𝑝 ∈ 𝐴 ∧ 𝑝 ( 2nd ↾ ( V × V ) ) 𝑥 ) )
36	33 34 35	3bitr4i	⊢ ( 𝑥 ∈ ran 𝐴 ↔ 𝑥 ∈ ( ( 2nd ↾ ( V × V ) ) “ 𝐴 ) )
37	36	eqriv	⊢ ran 𝐴 = ( ( 2nd ↾ ( V × V ) ) “ 𝐴 )