Theorem 2nd2val

Description: Value of an alternate definition of the 2nd function. (Contributed by NM, 10-Aug-2006) (Revised by Mario Carneiro, 30-Dec-2014)

	Ref	Expression
Assertion	2nd2val	⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ( 2nd ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elvv	⊢ ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑤 ∃ 𝑣 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ )
2		fveq2	⊢ ( 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ ⟨ 𝑤 , 𝑣 ⟩ ) )
3		df-ov	⊢ ( 𝑤 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } 𝑣 ) = ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ ⟨ 𝑤 , 𝑣 ⟩ )
4		simpr	⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑣 ) → 𝑦 = 𝑣 )
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	12 7	op2ndd	⊢ ( 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( 2nd ‘ 𝐴 ) = 𝑣 )
14	11 13	eqtr4d	⊢ ( 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ( 2nd ‘ 𝐴 ) )
15	14	exlimivv	⊢ ( ∃ 𝑤 ∃ 𝑣 𝐴 = ⟨ 𝑤 , 𝑣 ⟩ → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ( 2nd ‘ 𝐴 ) )
16	1 15	sylbi	⊢ ( 𝐴 ∈ ( V × V ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ( 2nd ‘ 𝐴 ) )
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		rnsnn0	⊢ ( 𝐴 ∈ ( V × V ) ↔ ran { 𝐴 } ≠ ∅ )
30	29	biimpri	⊢ ( ran { 𝐴 } ≠ ∅ → 𝐴 ∈ ( V × V ) )
31	30	necon1bi	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ran { 𝐴 } = ∅ )
32	31	unieqd	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ∪ ran { 𝐴 } = ∪ ∅ )
33		uni0	⊢ ∪ ∅ = ∅
34	32 33	eqtrdi	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ∪ ran { 𝐴 } = ∅ )
35	28 34	eqtr4d	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ∪ ran { 𝐴 } )
36		2ndval	⊢ ( 2nd ‘ 𝐴 ) = ∪ ran { 𝐴 }
37	35 36	eqtr4di	⊢ ( ¬ 𝐴 ∈ ( V × V ) → ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ( 2nd ‘ 𝐴 ) )
38	16 37	pm2.61i	⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑧 = 𝑦 } ‘ 𝐴 ) = ( 2nd ‘ 𝐴 )