Metamath Proof Explorer

Theorem f1o2ndf1

Description: The 2nd (second component of an ordered pair) function restricted to a one-to-one function F is a one-to-one function from F onto the range of F . (Contributed by Alexander van der Vekens, 4-Feb-2018)

Ref Expression
Assertion f1o2ndf1 ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 2nd ↾ 𝐹 ) : 𝐹 –1-1-onto→ ran 𝐹 )

Proof

Step Hyp Ref Expression
1 f1f ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 fo2ndf ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 2nd ↾ 𝐹 ) : 𝐹 –onto→ ran 𝐹 )
3 1 2 syl ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 2nd ↾ 𝐹 ) : 𝐹 –onto→ ran 𝐹 )
4 f2ndf ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 2nd ↾ 𝐹 ) : 𝐹 ⟶ 𝐵 )
5 1 4 syl ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 2nd ↾ 𝐹 ) : 𝐹 ⟶ 𝐵 )
6 fssxp ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 ⊆ ( 𝐴 × 𝐵 ) )
7 1 6 syl ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 ⊆ ( 𝐴 × 𝐵 ) )
8 ssel2 ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ∈ ( 𝐴 × 𝐵 ) )
9 elxp2 ⊢ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑣 ∈ 𝐵 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ )
10 8 9 sylib ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑣 ∈ 𝐵 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ )
11 ssel2 ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → 𝑦 ∈ ( 𝐴 × 𝐵 ) )
12 elxp2 ⊢ ( 𝑦 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑏 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ )
13 11 12 sylib ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ∃ 𝑏 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ )
14 10 13 anim12dan ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑣 ∈ 𝐵 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ∧ ∃ 𝑏 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ ) )
15 fvres ⊢ ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 → ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = ( 2nd ‘ ⟨ 𝑎 , 𝑣 ⟩ ) )
16 15 ad2antrr ⊢ ( ( ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = ( 2nd ‘ ⟨ 𝑎 , 𝑣 ⟩ ) )
17 fvres ⊢ ( ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 → ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑏 , 𝑤 ⟩ ) = ( 2nd ‘ ⟨ 𝑏 , 𝑤 ⟩ ) )
18 17 ad2antlr ⊢ ( ( ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑏 , 𝑤 ⟩ ) = ( 2nd ‘ ⟨ 𝑏 , 𝑤 ⟩ ) )
19 16 18 eqeq12d ⊢ ( ( ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑏 , 𝑤 ⟩ ) ↔ ( 2nd ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = ( 2nd ‘ ⟨ 𝑏 , 𝑤 ⟩ ) ) )
20 vex ⊢ 𝑎 ∈ V
21 vex ⊢ 𝑣 ∈ V
22 20 21 op2nd ⊢ ( 2nd ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = 𝑣
23 vex ⊢ 𝑏 ∈ V
24 vex ⊢ 𝑤 ∈ V
25 23 24 op2nd ⊢ ( 2nd ‘ ⟨ 𝑏 , 𝑤 ⟩ ) = 𝑤
26 22 25 eqeq12i ⊢ ( ( 2nd ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = ( 2nd ‘ ⟨ 𝑏 , 𝑤 ⟩ ) ↔ 𝑣 = 𝑤 )
27 f1fun ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → Fun 𝐹 )
28 funopfv ⊢ ( Fun 𝐹 → ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 → ( 𝐹 ‘ 𝑎 ) = 𝑣 ) )
29 funopfv ⊢ ( Fun 𝐹 → ( ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 → ( 𝐹 ‘ 𝑏 ) = 𝑤 ) )
30 28 29 anim12d ⊢ ( Fun 𝐹 → ( ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) → ( ( 𝐹 ‘ 𝑎 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑤 ) ) )
31 27 30 syl ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) → ( ( 𝐹 ‘ 𝑎 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑤 ) ) )
32 eqcom ⊢ ( ( 𝐹 ‘ 𝑎 ) = 𝑣 ↔ 𝑣 = ( 𝐹 ‘ 𝑎 ) )
33 32 biimpi ⊢ ( ( 𝐹 ‘ 𝑎 ) = 𝑣 → 𝑣 = ( 𝐹 ‘ 𝑎 ) )
34 eqcom ⊢ ( ( 𝐹 ‘ 𝑏 ) = 𝑤 ↔ 𝑤 = ( 𝐹 ‘ 𝑏 ) )
35 34 biimpi ⊢ ( ( 𝐹 ‘ 𝑏 ) = 𝑤 → 𝑤 = ( 𝐹 ‘ 𝑏 ) )
36 33 35 eqeqan12d ⊢ ( ( ( 𝐹 ‘ 𝑎 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑤 ) → ( 𝑣 = 𝑤 ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) )
37 simpl ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) → 𝑎 ∈ 𝐴 )
38 simpl ⊢ ( ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) → 𝑏 ∈ 𝐴 )
39 37 38 anim12i ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) )
40 f1veqaeq ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
41 39 40 sylan2 ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
42 opeq12 ⊢ ( ( 𝑎 = 𝑏 ∧ 𝑣 = 𝑤 ) → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ )
43 42 ex ⊢ ( 𝑎 = 𝑏 → ( 𝑣 = 𝑤 → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) )
44 41 43 syl6 ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → ( 𝑣 = 𝑤 → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) )
45 44 com23 ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑣 = 𝑤 → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) )
46 45 ex ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑣 = 𝑤 → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) ) )
47 46 com14 ⊢ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑣 = 𝑤 → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) ) )
48 36 47 biimtrdi ⊢ ( ( ( 𝐹 ‘ 𝑎 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑤 ) → ( 𝑣 = 𝑤 → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑣 = 𝑤 → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) ) ) )
49 48 com14 ⊢ ( 𝑣 = 𝑤 → ( 𝑣 = 𝑤 → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑤 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) ) ) )
50 49 pm2.43i ⊢ ( 𝑣 = 𝑤 → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑤 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) ) )
51 50 com14 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑤 ) → ( 𝑣 = 𝑤 → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) ) )
52 51 com23 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 𝐹 ‘ 𝑎 ) = 𝑣 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑤 ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑣 = 𝑤 → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) ) )
53 31 52 syld ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑣 = 𝑤 → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) ) )
54 53 com13 ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝑣 = 𝑤 → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) ) )
55 54 impcom ⊢ ( ( ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝑣 = 𝑤 → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) )
56 55 com23 ⊢ ( ( ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝑣 = 𝑤 → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) )
57 26 56 biimtrid ⊢ ( ( ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( 2nd ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = ( 2nd ‘ ⟨ 𝑏 , 𝑤 ⟩ ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) )
58 19 57 sylbid ⊢ ( ( ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑏 , 𝑤 ⟩ ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) )
59 58 com23 ⊢ ( ( ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑏 , 𝑤 ⟩ ) → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) )
60 59 ex ⊢ ( ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑏 , 𝑤 ⟩ ) → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) ) )
61 60 adantl ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑏 , 𝑤 ⟩ ) → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) ) )
62 61 com12 ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑏 , 𝑤 ⟩ ) → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) ) )
63 62 ad4ant13 ⊢ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ ) → ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑏 , 𝑤 ⟩ ) → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) ) )
64 eleq1 ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ → ( 𝑥 ∈ 𝐹 ↔ ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ) )
65 64 ad2antlr ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐹 ↔ ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ) )
66 eleq1 ⊢ ( 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ → ( 𝑦 ∈ 𝐹 ↔ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) )
67 65 66 bi2anan9 ⊢ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ ) → ( ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ↔ ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) ) )
68 67 anbi2d ⊢ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ ) → ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) ↔ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) ) ) )
69 fveq2 ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ → ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑎 , 𝑣 ⟩ ) )
70 69 ad2antlr ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑎 , 𝑣 ⟩ ) )
71 fveq2 ⊢ ( 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ → ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) = ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑏 , 𝑤 ⟩ ) )
72 70 71 eqeqan12d ⊢ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ ) → ( ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) ↔ ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑏 , 𝑤 ⟩ ) ) )
73 simpllr ⊢ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ ) → 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ )
74 simpr ⊢ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ ) → 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ )
75 73 74 eqeq12d ⊢ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ ) → ( 𝑥 = 𝑦 ↔ ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) )
76 72 75 imbi12d ⊢ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ ) → ( ( ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑏 , 𝑤 ⟩ ) → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) )
77 76 imbi2d ⊢ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ ) → ( ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ↔ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑎 , 𝑣 ⟩ ) = ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑏 , 𝑤 ⟩ ) → ⟨ 𝑎 , 𝑣 ⟩ = ⟨ 𝑏 , 𝑤 ⟩ ) ) ) )
78 63 68 77 3imtr4d ⊢ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) ∧ 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ ) → ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
79 78 ex ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ → ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) ) )
80 79 rexlimdvva ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ) → ( ∃ 𝑏 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ → ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) ) )
81 80 ex ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) → ( 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ → ( ∃ 𝑏 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ → ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) ) ) )
82 81 rexlimivv ⊢ ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑣 ∈ 𝐵 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ → ( ∃ 𝑏 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ → ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) ) )
83 82 imp ⊢ ( ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑣 ∈ 𝐵 𝑥 = ⟨ 𝑎 , 𝑣 ⟩ ∧ ∃ 𝑏 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑦 = ⟨ 𝑏 , 𝑤 ⟩ ) → ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
84 14 83 mpcom ⊢ ( ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
85 84 ex ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
86 85 com23 ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) )
87 7 86 mpcom ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
88 87 ralrimivv ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
89 dff13 ⊢ ( ( 2nd ↾ 𝐹 ) : 𝐹 –1-1→ 𝐵 ↔ ( ( 2nd ↾ 𝐹 ) : 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( ( ( 2nd ↾ 𝐹 ) ‘ 𝑥 ) = ( ( 2nd ↾ 𝐹 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
90 5 88 89 sylanbrc ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 2nd ↾ 𝐹 ) : 𝐹 –1-1→ 𝐵 )
91 df-f1 ⊢ ( ( 2nd ↾ 𝐹 ) : 𝐹 –1-1→ 𝐵 ↔ ( ( 2nd ↾ 𝐹 ) : 𝐹 ⟶ 𝐵 ∧ Fun ◡ ( 2nd ↾ 𝐹 ) ) )
92 91 simprbi ⊢ ( ( 2nd ↾ 𝐹 ) : 𝐹 –1-1→ 𝐵 → Fun ◡ ( 2nd ↾ 𝐹 ) )
93 90 92 syl ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → Fun ◡ ( 2nd ↾ 𝐹 ) )
94 dff1o3 ⊢ ( ( 2nd ↾ 𝐹 ) : 𝐹 –1-1-onto→ ran 𝐹 ↔ ( ( 2nd ↾ 𝐹 ) : 𝐹 –onto→ ran 𝐹 ∧ Fun ◡ ( 2nd ↾ 𝐹 ) ) )
95 3 93 94 sylanbrc ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 2nd ↾ 𝐹 ) : 𝐹 –1-1-onto→ ran 𝐹 )