Metamath Proof Explorer

Theorem fv2ndcnv

Description: The value of the converse of 2nd restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020)

Ref Expression
Assertion fv2ndcnv ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ‘ 𝑌 ) = ⟨ 𝑋 , 𝑌 ⟩ )

Proof

Step Hyp Ref Expression
1 snidg ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ { 𝑋 } )
2 1 anim1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) )
3 eqid ⊢ 𝑌 = 𝑌
4 2 3 jctir ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑌 = 𝑌 ) )
5 2ndconst ⊢ ( 𝑋 ∈ 𝑉 → ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) : ( { 𝑋 } × 𝐴 ) –1-1-onto→ 𝐴 )
6 5 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) : ( { 𝑋 } × 𝐴 ) –1-1-onto→ 𝐴 )
7 f1ocnv ⊢ ( ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) : ( { 𝑋 } × 𝐴 ) –1-1-onto→ 𝐴 → ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) : 𝐴 –1-1-onto→ ( { 𝑋 } × 𝐴 ) )
8 f1ofn ⊢ ( ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) : 𝐴 –1-1-onto→ ( { 𝑋 } × 𝐴 ) → ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) Fn 𝐴 )
9 6 7 8 3syl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) Fn 𝐴 )
10 fnbrfvb ⊢ ( ( ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) Fn 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ‘ 𝑌 ) = ⟨ 𝑋 , 𝑌 ⟩ ↔ 𝑌 ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ⟨ 𝑋 , 𝑌 ⟩ ) )
11 9 10 sylancom ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ( ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ‘ 𝑌 ) = ⟨ 𝑋 , 𝑌 ⟩ ↔ 𝑌 ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ⟨ 𝑋 , 𝑌 ⟩ ) )
12 opex ⊢ ⟨ 𝑋 , 𝑌 ⟩ ∈ V
13 brcnvg ⊢ ( ( 𝑌 ∈ 𝐴 ∧ ⟨ 𝑋 , 𝑌 ⟩ ∈ V ) → ( 𝑌 ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ⟨ 𝑋 , 𝑌 ⟩ ↔ ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 𝑌 ) )
14 12 13 mpan2 ⊢ ( 𝑌 ∈ 𝐴 → ( 𝑌 ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ⟨ 𝑋 , 𝑌 ⟩ ↔ ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 𝑌 ) )
15 14 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ⟨ 𝑋 , 𝑌 ⟩ ↔ ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 𝑌 ) )
16 brres ⊢ ( 𝑌 ∈ 𝐴 → ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 𝑌 ↔ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( { 𝑋 } × 𝐴 ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 2nd 𝑌 ) ) )
17 16 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 𝑌 ↔ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( { 𝑋 } × 𝐴 ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 2nd 𝑌 ) ) )
18 opelxp ⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( { 𝑋 } × 𝐴 ) ↔ ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) )
19 18 anbi1i ⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( { 𝑋 } × 𝐴 ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 2nd 𝑌 ) ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 2nd 𝑌 ) )
20 br2ndeqg ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ⟨ 𝑋 , 𝑌 ⟩ 2nd 𝑌 ↔ 𝑌 = 𝑌 ) )
21 20 anbi2d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 2nd 𝑌 ) ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑌 = 𝑌 ) ) )
22 19 21 bitrid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( { 𝑋 } × 𝐴 ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 2nd 𝑌 ) ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑌 = 𝑌 ) ) )
23 17 22 bitrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 𝑌 ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑌 = 𝑌 ) ) )
24 15 23 bitrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ⟨ 𝑋 , 𝑌 ⟩ ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑌 = 𝑌 ) ) )
25 11 24 bitrd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ( ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ‘ 𝑌 ) = ⟨ 𝑋 , 𝑌 ⟩ ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑌 = 𝑌 ) ) )
26 4 25 mpbird ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ‘ 𝑌 ) = ⟨ 𝑋 , 𝑌 ⟩ )