Theorem 1st2val

Description: Value of an alternate definition of the 1st function. (Contributed by NM, 14-Oct-2004) (Revised by Mario Carneiro, 30-Dec-2014)

	Ref	Expression
Assertion	1st2val	⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ( 1st ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elvv	⊢ ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑤 ∃ 𝑣 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ )
2		fveq2	⊢ ( 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ ⟨ 𝑤 , 𝑣 ⟩ ) )
3		df-ov	⊢ ( 𝑤 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } 𝑣 ) = ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ ⟨ 𝑤 , 𝑣 ⟩ )
4		simpl	⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑣 ) → 𝑥 = 𝑤 )
5		mpov	⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ 𝑥 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 }
6	5	eqcomi	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ 𝑥 )
7		vex	⊢ 𝑤 ∈ V
8	4 6 7	ovmpoa	⊢ ( ( 𝑤 ∈ V ∧ 𝑣 ∈ V ) → ( 𝑤 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } 𝑣 ) = 𝑤 )
9	8	el2v	⊢ ( 𝑤 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } 𝑣 ) = 𝑤
10	3 9	eqtr3i	⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ ⟨ 𝑤 , 𝑣 ⟩ ) = 𝑤
11	2 10	eqtrdi	⊢ ( 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = 𝑤 )
12		vex	⊢ 𝑣 ∈ V
13	7 12	op1std	⊢ ( 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( 1st ‘ 𝐴 ) = 𝑤 )
14	11 13	eqtr4d	⊢ ( 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ( 1st ‘ 𝐴 ) )
15	14	exlimivv	⊢ ( ∃ 𝑤 ∃ 𝑣 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ( 1st ‘ 𝐴 ) )
16	1 15	sylbi	⊢ ( 𝐴 ∈ ( V × V ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ( 1st ‘ 𝐴 ) )
17		vex	⊢ 𝑥 ∈ V
18		vex	⊢ 𝑦 ∈ V
19	17 18	pm3.2i	⊢ ( 𝑥 ∈ V ∧ 𝑦 ∈ V )
20		ax6ev	⊢ ∃ 𝑧 𝑧 = 𝑥
21	19 20	2th	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ↔ ∃ 𝑧 𝑧 = 𝑥 )
22	21	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 𝑧 = 𝑥 }
23		df-xp	⊢ ( V × V ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) }
24		dmoprab	⊢ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 𝑧 = 𝑥 }
25	22 23 24	3eqtr4ri	⊢ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } = ( V × V )
26	25	eleq2i	⊢ ( 𝐴 ∈ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ↔ 𝐴 ∈ ( V × V ) )
27		ndmfv	⊢ ( ¬ 𝐴 ∈ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ∅ )
28	26 27	sylnbir	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ∅ )
29		dmsnn0	⊢ ( 𝐴 ∈ ( V × V ) ↔ dom { 𝐴 } ≠ ∅ )
30	29	biimpri	⊢ ( dom { 𝐴 } ≠ ∅ → 𝐴 ∈ ( V × V ) )
31	30	necon1bi	⊢ ( ¬ 𝐴 ∈ ( V × V ) → dom { 𝐴 } = ∅ )
32	31	unieqd	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ∪ dom { 𝐴 } = ∪ ∅ )
33		uni0	⊢ ∪ ∅ = ∅
34	32 33	eqtrdi	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ∪ dom { 𝐴 } = ∅ )
35	28 34	eqtr4d	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ∪ dom { 𝐴 } )
36		1stval	⊢ ( 1st ‘ 𝐴 ) = ∪ dom { 𝐴 }
37	35 36	eqtr4di	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ( 1st ‘ 𝐴 ) )
38	16 37	pm2.61i	⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑥 } ‘ 𝐴 ) = ( 1st ‘ 𝐴 )