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 syl6bi ( ( ( 𝐹𝑎 ) = 𝑣 ∧ ( 𝐹𝑏 ) = 𝑤 ) → ( 𝑣 = 𝑤 → ( ( ( 𝑎𝐴𝑣𝐵 ) ∧ ( 𝑏𝐴𝑤𝐵 ) ) → ( 𝑣 = 𝑤 → ( 𝐹 : 𝐴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 syl5bi ( ( ( ⟨ 𝑎 , 𝑣 ⟩ ∈ 𝐹 ∧ ⟨ 𝑏 , 𝑤 ⟩ ∈ 𝐹 ) ∧ ( ( 𝑎𝐴𝑣𝐵 ) ∧ ( 𝑏𝐴𝑤𝐵 ) ) ) → ( ( 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 𝐹 )