Metamath Proof Explorer

Theorem onelfvnef1

Description: A sufficient condition for a function on ordinals to be one-to-one. (Contributed by NM, 9-Feb-1997) Extract from tz7.48lem and generalize statement. (Revised by Matthew House, 6-Sep-2026)

Ref Expression
Assertion onelfvnef1 ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) → 𝐹 : 𝐴 –1-1→ 𝐵 )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
2 elequ12 ⊢ ( ( 𝑦 = 𝑧 ∧ 𝑥 = 𝑤 ) → ( 𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤 ) )
3 2 ancoms ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( 𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤 ) )
4 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
5 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
6 4 5 eqeqan12d ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ) )
7 6 necon3bid ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑤 ) ≠ ( 𝐹 ‘ 𝑧 ) ) )
8 3 7 imbi12d ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) ≠ ( 𝐹 ‘ 𝑧 ) ) ) )
9 8 rspc2gv ⊢ ( ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) → ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) ≠ ( 𝐹 ‘ 𝑧 ) ) ) )
10 9 ancoms ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) → ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) ≠ ( 𝐹 ‘ 𝑧 ) ) ) )
11 10 impcom ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) ≠ ( 𝐹 ‘ 𝑧 ) ) )
12 necom ⊢ ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑤 ) ≠ ( 𝐹 ‘ 𝑧 ) )
13 11 12 imbitrrdi ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) ) )
14 elequ12 ⊢ ( ( 𝑦 = 𝑤 ∧ 𝑥 = 𝑧 ) → ( 𝑦 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) )
15 14 ancoms ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑦 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) )
16 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
17 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑤 ) )
18 16 17 eqeqan12d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) )
19 18 necon3bid ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) ) )
20 15 19 imbi12d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑤 ∈ 𝑧 → ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) ) ) )
21 20 rspc2gv ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) → ( 𝑤 ∈ 𝑧 → ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) ) ) )
22 21 impcom ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑤 ∈ 𝑧 → ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) ) )
23 13 22 jaod ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧 ) → ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) ) )
24 23 necon2bd ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → ¬ ( 𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧 ) ) )
25 24 3ad2antl3 ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → ¬ ( 𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧 ) ) )
26 ssel2 ⊢ ( ( 𝐴 ⊆ On ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ On )
27 ssel2 ⊢ ( ( 𝐴 ⊆ On ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ On )
28 eloni ⊢ ( 𝑧 ∈ On → Ord 𝑧 )
29 eloni ⊢ ( 𝑤 ∈ On → Ord 𝑤 )
30 ordtri3 ⊢ ( ( Ord 𝑧 ∧ Ord 𝑤 ) → ( 𝑧 = 𝑤 ↔ ¬ ( 𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧 ) ) )
31 28 29 30 syl2an ⊢ ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( 𝑧 = 𝑤 ↔ ¬ ( 𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧 ) ) )
32 26 27 31 syl2an ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐴 ⊆ On ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 = 𝑤 ↔ ¬ ( 𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧 ) ) )
33 32 anandis ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 = 𝑤 ↔ ¬ ( 𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧 ) ) )
34 33 3ad2antl2 ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 = 𝑤 ↔ ¬ ( 𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧 ) ) )
35 25 34 sylibrd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
36 35 ralrimivva ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
37 dff13 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
38 1 36 37 sylanbrc ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ On ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑦 ) ) ) → 𝐹 : 𝐴 –1-1→ 𝐵 )