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

Metamath Proof Explorer

Theorem smo11

Description: A strictly monotone ordinal function is one-to-one. (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion smo11 ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Smo 𝐹 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Smo 𝐹 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
2 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
3 smodm2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → Ord 𝐴 )
4 ordelord ⊢ ( ( Ord 𝐴 ∧ 𝑧 ∈ 𝐴 ) → Ord 𝑧 )
5 4 ex ⊢ ( Ord 𝐴 → ( 𝑧 ∈ 𝐴 → Ord 𝑧 ) )
6 3 5 syl ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → ( 𝑧 ∈ 𝐴 → Ord 𝑧 ) )
7 ordelord ⊢ ( ( Ord 𝐴 ∧ 𝑤 ∈ 𝐴 ) → Ord 𝑤 )
8 7 ex ⊢ ( Ord 𝐴 → ( 𝑤 ∈ 𝐴 → Ord 𝑤 ) )
9 3 8 syl ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → ( 𝑤 ∈ 𝐴 → Ord 𝑤 ) )
10 6 9 anim12d ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( Ord 𝑧 ∧ Ord 𝑤 ) ) )
11 ordtri3or ⊢ ( ( Ord 𝑧 ∧ Ord 𝑤 ) → ( 𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧 ) )
12 simp1rr ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝑤 ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → 𝑤 ∈ 𝐴 )
13 smoel2 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) )
14 13 ralrimivva ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) )
15 14 adantr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) )
16 15 3ad2ant1 ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝑤 ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) )
17 simp2 ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝑤 ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → 𝑧 ∈ 𝑤 )
18 simp3 ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝑤 ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) )
19 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
20 19 eleq2d ⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑤 ) ) )
21 20 raleqbi1dv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑤 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑤 ) ) )
22 21 rspcv ⊢ ( 𝑤 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) → ∀ 𝑦 ∈ 𝑤 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑤 ) ) )
23 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
24 23 eleq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) )
25 24 rspccv ⊢ ( ∀ 𝑦 ∈ 𝑤 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑤 ) → ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) )
26 22 25 syl6 ⊢ ( 𝑤 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) → ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) ) )
27 26 3imp ⊢ ( ( 𝑤 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 ∈ 𝑤 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) )
28 eleq1 ⊢ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) ) )
29 28 biimpac ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) )
30 27 29 sylan ⊢ ( ( ( 𝑤 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) )
31 12 16 17 18 30 syl31anc ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝑤 ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) )
32 smofvon2 ⊢ ( Smo 𝐹 → ( 𝐹 ‘ 𝑤 ) ∈ On )
33 eloni ⊢ ( ( 𝐹 ‘ 𝑤 ) ∈ On → Ord ( 𝐹 ‘ 𝑤 ) )
34 ordirr ⊢ ( Ord ( 𝐹 ‘ 𝑤 ) → ¬ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) )
35 32 33 34 3syl ⊢ ( Smo 𝐹 → ¬ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) )
36 35 ad2antlr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ¬ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) )
37 36 3ad2ant1 ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝑤 ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ¬ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) )
38 31 37 pm2.21dd ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝑤 ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → 𝑧 = 𝑤 )
39 38 3exp ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 ∈ 𝑤 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
40 ax-1 ⊢ ( 𝑧 = 𝑤 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
41 40 a1i ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 = 𝑤 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
42 simp1rl ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ 𝑤 ∈ 𝑧 ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → 𝑧 ∈ 𝐴 )
43 15 3ad2ant1 ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ 𝑤 ∈ 𝑧 ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) )
44 simp2 ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ 𝑤 ∈ 𝑧 ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → 𝑤 ∈ 𝑧 )
45 simp3 ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ 𝑤 ∈ 𝑧 ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) )
46 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
47 46 eleq2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ) )
48 47 raleqbi1dv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑧 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ) )
49 48 rspcv ⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) → ∀ 𝑦 ∈ 𝑧 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ) )
50 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑤 ) )
51 50 eleq1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) ) )
52 51 rspccv ⊢ ( ∀ 𝑦 ∈ 𝑧 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑧 ) → ( 𝑤 ∈ 𝑧 → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) ) )
53 49 52 syl6 ⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) → ( 𝑤 ∈ 𝑧 → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) ) ) )
54 53 3imp ⊢ ( ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ 𝑧 ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) )
55 eleq2 ⊢ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) ) )
56 55 biimpac ⊢ ( ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) )
57 54 56 sylan ⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ 𝑧 ) ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) )
58 42 43 44 45 57 syl31anc ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ 𝑤 ∈ 𝑧 ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) )
59 36 3ad2ant1 ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ 𝑤 ∈ 𝑧 ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → ¬ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) )
60 58 59 pm2.21dd ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ 𝑤 ∈ 𝑧 ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) → 𝑧 = 𝑤 )
61 60 3exp ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑤 ∈ 𝑧 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
62 39 41 61 3jaod ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
63 11 62 syl5 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( Ord 𝑧 ∧ Ord 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
64 63 ex ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ( Ord 𝑧 ∧ Ord 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) ) )
65 10 64 mpdd ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
66 65 ralrimivv ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
67 2 66 sylan ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Smo 𝐹 ) → ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
68 dff13 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
69 1 67 68 sylanbrc ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Smo 𝐹 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )