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 syl5bb ( ( 𝑋𝑉𝑌𝐴 ) → ( ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( { 𝑋 } × 𝐴 ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 2nd 𝑌 ) ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌𝐴 ) ∧ 𝑌 = 𝑌 ) ) )
23 17 22 bitrd ( ( 𝑋𝑉𝑌𝐴 ) → ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 𝑌 ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌𝐴 ) ∧ 𝑌 = 𝑌 ) ) )
24 15 23 bitrd ( ( 𝑋𝑉𝑌𝐴 ) → ( 𝑌 ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ⟨ 𝑋 , 𝑌 ⟩ ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌𝐴 ) ∧ 𝑌 = 𝑌 ) ) )
25 11 24 bitrd ( ( 𝑋𝑉𝑌𝐴 ) → ( ( ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ‘ 𝑌 ) = ⟨ 𝑋 , 𝑌 ⟩ ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌𝐴 ) ∧ 𝑌 = 𝑌 ) ) )
26 4 25 mpbird ( ( 𝑋𝑉𝑌𝐴 ) → ( ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ‘ 𝑌 ) = ⟨ 𝑋 , 𝑌 ⟩ )