Metamath Proof Explorer


Theorem 2ndconst

Description: The mapping of a restriction of the 2nd function to a converse constant function. (Contributed by NM, 27-Mar-2008) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion 2ndconst ( 𝐴𝑉 → ( 2nd ↾ ( { 𝐴 } × 𝐵 ) ) : ( { 𝐴 } × 𝐵 ) –1-1-onto𝐵 )

Proof

Step Hyp Ref Expression
1 snnzg ( 𝐴𝑉 → { 𝐴 } ≠ ∅ )
2 fo2ndres ( { 𝐴 } ≠ ∅ → ( 2nd ↾ ( { 𝐴 } × 𝐵 ) ) : ( { 𝐴 } × 𝐵 ) –onto𝐵 )
3 1 2 syl ( 𝐴𝑉 → ( 2nd ↾ ( { 𝐴 } × 𝐵 ) ) : ( { 𝐴 } × 𝐵 ) –onto𝐵 )
4 moeq ∃* 𝑥 𝑥 = ⟨ 𝐴 , 𝑦
5 4 moani ∃* 𝑥 ( 𝑦𝐵𝑥 = ⟨ 𝐴 , 𝑦 ⟩ )
6 vex 𝑦 ∈ V
7 6 brresi ( 𝑥 ( 2nd ↾ ( { 𝐴 } × 𝐵 ) ) 𝑦 ↔ ( 𝑥 ∈ ( { 𝐴 } × 𝐵 ) ∧ 𝑥 2nd 𝑦 ) )
8 fo2nd 2nd : V –onto→ V
9 fofn ( 2nd : V –onto→ V → 2nd Fn V )
10 8 9 ax-mp 2nd Fn V
11 vex 𝑥 ∈ V
12 fnbrfvb ( ( 2nd Fn V ∧ 𝑥 ∈ V ) → ( ( 2nd𝑥 ) = 𝑦𝑥 2nd 𝑦 ) )
13 10 11 12 mp2an ( ( 2nd𝑥 ) = 𝑦𝑥 2nd 𝑦 )
14 13 anbi2i ( ( 𝑥 ∈ ( { 𝐴 } × 𝐵 ) ∧ ( 2nd𝑥 ) = 𝑦 ) ↔ ( 𝑥 ∈ ( { 𝐴 } × 𝐵 ) ∧ 𝑥 2nd 𝑦 ) )
15 elxp7 ( 𝑥 ∈ ( { 𝐴 } × 𝐵 ) ↔ ( 𝑥 ∈ ( V × V ) ∧ ( ( 1st𝑥 ) ∈ { 𝐴 } ∧ ( 2nd𝑥 ) ∈ 𝐵 ) ) )
16 eleq1 ( ( 2nd𝑥 ) = 𝑦 → ( ( 2nd𝑥 ) ∈ 𝐵𝑦𝐵 ) )
17 16 biimpac ( ( ( 2nd𝑥 ) ∈ 𝐵 ∧ ( 2nd𝑥 ) = 𝑦 ) → 𝑦𝐵 )
18 17 adantll ( ( ( ( 1st𝑥 ) ∈ { 𝐴 } ∧ ( 2nd𝑥 ) ∈ 𝐵 ) ∧ ( 2nd𝑥 ) = 𝑦 ) → 𝑦𝐵 )
19 18 adantll ( ( ( 𝑥 ∈ ( V × V ) ∧ ( ( 1st𝑥 ) ∈ { 𝐴 } ∧ ( 2nd𝑥 ) ∈ 𝐵 ) ) ∧ ( 2nd𝑥 ) = 𝑦 ) → 𝑦𝐵 )
20 elsni ( ( 1st𝑥 ) ∈ { 𝐴 } → ( 1st𝑥 ) = 𝐴 )
21 eqopi ( ( 𝑥 ∈ ( V × V ) ∧ ( ( 1st𝑥 ) = 𝐴 ∧ ( 2nd𝑥 ) = 𝑦 ) ) → 𝑥 = ⟨ 𝐴 , 𝑦 ⟩ )
22 21 anassrs ( ( ( 𝑥 ∈ ( V × V ) ∧ ( 1st𝑥 ) = 𝐴 ) ∧ ( 2nd𝑥 ) = 𝑦 ) → 𝑥 = ⟨ 𝐴 , 𝑦 ⟩ )
23 20 22 sylanl2 ( ( ( 𝑥 ∈ ( V × V ) ∧ ( 1st𝑥 ) ∈ { 𝐴 } ) ∧ ( 2nd𝑥 ) = 𝑦 ) → 𝑥 = ⟨ 𝐴 , 𝑦 ⟩ )
24 23 adantlrr ( ( ( 𝑥 ∈ ( V × V ) ∧ ( ( 1st𝑥 ) ∈ { 𝐴 } ∧ ( 2nd𝑥 ) ∈ 𝐵 ) ) ∧ ( 2nd𝑥 ) = 𝑦 ) → 𝑥 = ⟨ 𝐴 , 𝑦 ⟩ )
25 19 24 jca ( ( ( 𝑥 ∈ ( V × V ) ∧ ( ( 1st𝑥 ) ∈ { 𝐴 } ∧ ( 2nd𝑥 ) ∈ 𝐵 ) ) ∧ ( 2nd𝑥 ) = 𝑦 ) → ( 𝑦𝐵𝑥 = ⟨ 𝐴 , 𝑦 ⟩ ) )
26 15 25 sylanb ( ( 𝑥 ∈ ( { 𝐴 } × 𝐵 ) ∧ ( 2nd𝑥 ) = 𝑦 ) → ( 𝑦𝐵𝑥 = ⟨ 𝐴 , 𝑦 ⟩ ) )
27 26 adantl ( ( 𝐴𝑉 ∧ ( 𝑥 ∈ ( { 𝐴 } × 𝐵 ) ∧ ( 2nd𝑥 ) = 𝑦 ) ) → ( 𝑦𝐵𝑥 = ⟨ 𝐴 , 𝑦 ⟩ ) )
28 simprr ( ( 𝐴𝑉 ∧ ( 𝑦𝐵𝑥 = ⟨ 𝐴 , 𝑦 ⟩ ) ) → 𝑥 = ⟨ 𝐴 , 𝑦 ⟩ )
29 snidg ( 𝐴𝑉𝐴 ∈ { 𝐴 } )
30 29 adantr ( ( 𝐴𝑉 ∧ ( 𝑦𝐵𝑥 = ⟨ 𝐴 , 𝑦 ⟩ ) ) → 𝐴 ∈ { 𝐴 } )
31 simprl ( ( 𝐴𝑉 ∧ ( 𝑦𝐵𝑥 = ⟨ 𝐴 , 𝑦 ⟩ ) ) → 𝑦𝐵 )
32 30 31 opelxpd ( ( 𝐴𝑉 ∧ ( 𝑦𝐵𝑥 = ⟨ 𝐴 , 𝑦 ⟩ ) ) → ⟨ 𝐴 , 𝑦 ⟩ ∈ ( { 𝐴 } × 𝐵 ) )
33 28 32 eqeltrd ( ( 𝐴𝑉 ∧ ( 𝑦𝐵𝑥 = ⟨ 𝐴 , 𝑦 ⟩ ) ) → 𝑥 ∈ ( { 𝐴 } × 𝐵 ) )
34 fveq2 ( 𝑥 = ⟨ 𝐴 , 𝑦 ⟩ → ( 2nd𝑥 ) = ( 2nd ‘ ⟨ 𝐴 , 𝑦 ⟩ ) )
35 op2ndg ( ( 𝐴𝑉𝑦 ∈ V ) → ( 2nd ‘ ⟨ 𝐴 , 𝑦 ⟩ ) = 𝑦 )
36 35 elvd ( 𝐴𝑉 → ( 2nd ‘ ⟨ 𝐴 , 𝑦 ⟩ ) = 𝑦 )
37 34 36 sylan9eqr ( ( 𝐴𝑉𝑥 = ⟨ 𝐴 , 𝑦 ⟩ ) → ( 2nd𝑥 ) = 𝑦 )
38 37 adantrl ( ( 𝐴𝑉 ∧ ( 𝑦𝐵𝑥 = ⟨ 𝐴 , 𝑦 ⟩ ) ) → ( 2nd𝑥 ) = 𝑦 )
39 33 38 jca ( ( 𝐴𝑉 ∧ ( 𝑦𝐵𝑥 = ⟨ 𝐴 , 𝑦 ⟩ ) ) → ( 𝑥 ∈ ( { 𝐴 } × 𝐵 ) ∧ ( 2nd𝑥 ) = 𝑦 ) )
40 27 39 impbida ( 𝐴𝑉 → ( ( 𝑥 ∈ ( { 𝐴 } × 𝐵 ) ∧ ( 2nd𝑥 ) = 𝑦 ) ↔ ( 𝑦𝐵𝑥 = ⟨ 𝐴 , 𝑦 ⟩ ) ) )
41 14 40 bitr3id ( 𝐴𝑉 → ( ( 𝑥 ∈ ( { 𝐴 } × 𝐵 ) ∧ 𝑥 2nd 𝑦 ) ↔ ( 𝑦𝐵𝑥 = ⟨ 𝐴 , 𝑦 ⟩ ) ) )
42 7 41 syl5bb ( 𝐴𝑉 → ( 𝑥 ( 2nd ↾ ( { 𝐴 } × 𝐵 ) ) 𝑦 ↔ ( 𝑦𝐵𝑥 = ⟨ 𝐴 , 𝑦 ⟩ ) ) )
43 42 mobidv ( 𝐴𝑉 → ( ∃* 𝑥 𝑥 ( 2nd ↾ ( { 𝐴 } × 𝐵 ) ) 𝑦 ↔ ∃* 𝑥 ( 𝑦𝐵𝑥 = ⟨ 𝐴 , 𝑦 ⟩ ) ) )
44 5 43 mpbiri ( 𝐴𝑉 → ∃* 𝑥 𝑥 ( 2nd ↾ ( { 𝐴 } × 𝐵 ) ) 𝑦 )
45 44 alrimiv ( 𝐴𝑉 → ∀ 𝑦 ∃* 𝑥 𝑥 ( 2nd ↾ ( { 𝐴 } × 𝐵 ) ) 𝑦 )
46 funcnv2 ( Fun ( 2nd ↾ ( { 𝐴 } × 𝐵 ) ) ↔ ∀ 𝑦 ∃* 𝑥 𝑥 ( 2nd ↾ ( { 𝐴 } × 𝐵 ) ) 𝑦 )
47 45 46 sylibr ( 𝐴𝑉 → Fun ( 2nd ↾ ( { 𝐴 } × 𝐵 ) ) )
48 dff1o3 ( ( 2nd ↾ ( { 𝐴 } × 𝐵 ) ) : ( { 𝐴 } × 𝐵 ) –1-1-onto𝐵 ↔ ( ( 2nd ↾ ( { 𝐴 } × 𝐵 ) ) : ( { 𝐴 } × 𝐵 ) –onto𝐵 ∧ Fun ( 2nd ↾ ( { 𝐴 } × 𝐵 ) ) ) )
49 3 47 48 sylanbrc ( 𝐴𝑉 → ( 2nd ↾ ( { 𝐴 } × 𝐵 ) ) : ( { 𝐴 } × 𝐵 ) –1-1-onto𝐵 )