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

Proof

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