This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ( 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→ 𝐵 )