Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. 2
⊢ ((𝐹:𝐴⟶𝐵 ∧ Smo 𝐹) → 𝐹:𝐴⟶𝐵) |
2 | | ffn 6498 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
3 | | smodm2 8014 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → Ord 𝐴) |
4 | | ordelord 6188 |
. . . . . . . 8
⊢ ((Ord
𝐴 ∧ 𝑧 ∈ 𝐴) → Ord 𝑧) |
5 | 4 | ex 416 |
. . . . . . 7
⊢ (Ord
𝐴 → (𝑧 ∈ 𝐴 → Ord 𝑧)) |
6 | 3, 5 | syl 17 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → (𝑧 ∈ 𝐴 → Ord 𝑧)) |
7 | | ordelord 6188 |
. . . . . . . 8
⊢ ((Ord
𝐴 ∧ 𝑤 ∈ 𝐴) → Ord 𝑤) |
8 | 7 | ex 416 |
. . . . . . 7
⊢ (Ord
𝐴 → (𝑤 ∈ 𝐴 → Ord 𝑤)) |
9 | 3, 8 | syl 17 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → (𝑤 ∈ 𝐴 → Ord 𝑤)) |
10 | 6, 9 | anim12d 612 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (Ord 𝑧 ∧ Ord 𝑤))) |
11 | | ordtri3or 6198 |
. . . . . . 7
⊢ ((Ord
𝑧 ∧ Ord 𝑤) → (𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧)) |
12 | | simp1rr 1240 |
. . . . . . . . . . 11
⊢ ((((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ 𝑧 ∈ 𝑤 ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → 𝑤 ∈ 𝐴) |
13 | | smoel2 8022 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥)) → (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
14 | 13 | ralrimivva 3103 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
15 | 14 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
16 | 15 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ 𝑧 ∈ 𝑤 ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
17 | | simp2 1138 |
. . . . . . . . . . 11
⊢ ((((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ 𝑧 ∈ 𝑤 ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → 𝑧 ∈ 𝑤) |
18 | | simp3 1139 |
. . . . . . . . . . 11
⊢ ((((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ 𝑧 ∈ 𝑤 ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → (𝐹‘𝑧) = (𝐹‘𝑤)) |
19 | | fveq2 6668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤)) |
20 | 19 | eleq2d 2818 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑤 → ((𝐹‘𝑦) ∈ (𝐹‘𝑥) ↔ (𝐹‘𝑦) ∈ (𝐹‘𝑤))) |
21 | 20 | raleqbi1dv 3307 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → (∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥) ↔ ∀𝑦 ∈ 𝑤 (𝐹‘𝑦) ∈ (𝐹‘𝑤))) |
22 | 21 | rspcv 3519 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥) → ∀𝑦 ∈ 𝑤 (𝐹‘𝑦) ∈ (𝐹‘𝑤))) |
23 | | fveq2 6668 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧)) |
24 | 23 | eleq1d 2817 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦) ∈ (𝐹‘𝑤) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑤))) |
25 | 24 | rspccv 3521 |
. . . . . . . . . . . . . 14
⊢
(∀𝑦 ∈
𝑤 (𝐹‘𝑦) ∈ (𝐹‘𝑤) → (𝑧 ∈ 𝑤 → (𝐹‘𝑧) ∈ (𝐹‘𝑤))) |
26 | 22, 25 | syl6 35 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥) → (𝑧 ∈ 𝑤 → (𝐹‘𝑧) ∈ (𝐹‘𝑤)))) |
27 | 26 | 3imp 1112 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥) ∧ 𝑧 ∈ 𝑤) → (𝐹‘𝑧) ∈ (𝐹‘𝑤)) |
28 | | eleq1 2820 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑧) = (𝐹‘𝑤) → ((𝐹‘𝑧) ∈ (𝐹‘𝑤) ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑤))) |
29 | 28 | biimpac 482 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑧) ∈ (𝐹‘𝑤) ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → (𝐹‘𝑤) ∈ (𝐹‘𝑤)) |
30 | 27, 29 | sylan 583 |
. . . . . . . . . . 11
⊢ (((𝑤 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥) ∧ 𝑧 ∈ 𝑤) ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → (𝐹‘𝑤) ∈ (𝐹‘𝑤)) |
31 | 12, 16, 17, 18, 30 | syl31anc 1374 |
. . . . . . . . . 10
⊢ ((((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ 𝑧 ∈ 𝑤 ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → (𝐹‘𝑤) ∈ (𝐹‘𝑤)) |
32 | | smofvon2 8015 |
. . . . . . . . . . . . 13
⊢ (Smo
𝐹 → (𝐹‘𝑤) ∈ On) |
33 | | eloni 6176 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑤) ∈ On → Ord (𝐹‘𝑤)) |
34 | | ordirr 6184 |
. . . . . . . . . . . . 13
⊢ (Ord
(𝐹‘𝑤) → ¬ (𝐹‘𝑤) ∈ (𝐹‘𝑤)) |
35 | 32, 33, 34 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (Smo
𝐹 → ¬ (𝐹‘𝑤) ∈ (𝐹‘𝑤)) |
36 | 35 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ¬ (𝐹‘𝑤) ∈ (𝐹‘𝑤)) |
37 | 36 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ 𝑧 ∈ 𝑤 ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → ¬ (𝐹‘𝑤) ∈ (𝐹‘𝑤)) |
38 | 31, 37 | pm2.21dd 198 |
. . . . . . . . 9
⊢ ((((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ 𝑧 ∈ 𝑤 ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → 𝑧 = 𝑤) |
39 | 38 | 3exp 1120 |
. . . . . . . 8
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (𝑧 ∈ 𝑤 → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))) |
40 | | ax-1 6 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)) |
41 | 40 | a1i 11 |
. . . . . . . 8
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (𝑧 = 𝑤 → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))) |
42 | | simp1rl 1239 |
. . . . . . . . . . 11
⊢ ((((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ 𝑤 ∈ 𝑧 ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → 𝑧 ∈ 𝐴) |
43 | 15 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ 𝑤 ∈ 𝑧 ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) |
44 | | simp2 1138 |
. . . . . . . . . . 11
⊢ ((((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ 𝑤 ∈ 𝑧 ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → 𝑤 ∈ 𝑧) |
45 | | simp3 1139 |
. . . . . . . . . . 11
⊢ ((((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ 𝑤 ∈ 𝑧 ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → (𝐹‘𝑧) = (𝐹‘𝑤)) |
46 | | fveq2 6668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
47 | 46 | eleq2d 2818 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑦) ∈ (𝐹‘𝑥) ↔ (𝐹‘𝑦) ∈ (𝐹‘𝑧))) |
48 | 47 | raleqbi1dv 3307 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥) ↔ ∀𝑦 ∈ 𝑧 (𝐹‘𝑦) ∈ (𝐹‘𝑧))) |
49 | 48 | rspcv 3519 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥) → ∀𝑦 ∈ 𝑧 (𝐹‘𝑦) ∈ (𝐹‘𝑧))) |
50 | | fveq2 6668 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤)) |
51 | 50 | eleq1d 2817 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑤 → ((𝐹‘𝑦) ∈ (𝐹‘𝑧) ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑧))) |
52 | 51 | rspccv 3521 |
. . . . . . . . . . . . . 14
⊢
(∀𝑦 ∈
𝑧 (𝐹‘𝑦) ∈ (𝐹‘𝑧) → (𝑤 ∈ 𝑧 → (𝐹‘𝑤) ∈ (𝐹‘𝑧))) |
53 | 49, 52 | syl6 35 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥) → (𝑤 ∈ 𝑧 → (𝐹‘𝑤) ∈ (𝐹‘𝑧)))) |
54 | 53 | 3imp 1112 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ 𝑧) → (𝐹‘𝑤) ∈ (𝐹‘𝑧)) |
55 | | eleq2 2821 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑧) = (𝐹‘𝑤) → ((𝐹‘𝑤) ∈ (𝐹‘𝑧) ↔ (𝐹‘𝑤) ∈ (𝐹‘𝑤))) |
56 | 55 | biimpac 482 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑤) ∈ (𝐹‘𝑧) ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → (𝐹‘𝑤) ∈ (𝐹‘𝑤)) |
57 | 54, 56 | sylan 583 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ 𝑧) ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → (𝐹‘𝑤) ∈ (𝐹‘𝑤)) |
58 | 42, 43, 44, 45, 57 | syl31anc 1374 |
. . . . . . . . . 10
⊢ ((((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ 𝑤 ∈ 𝑧 ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → (𝐹‘𝑤) ∈ (𝐹‘𝑤)) |
59 | 36 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ 𝑤 ∈ 𝑧 ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → ¬ (𝐹‘𝑤) ∈ (𝐹‘𝑤)) |
60 | 58, 59 | pm2.21dd 198 |
. . . . . . . . 9
⊢ ((((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ 𝑤 ∈ 𝑧 ∧ (𝐹‘𝑧) = (𝐹‘𝑤)) → 𝑧 = 𝑤) |
61 | 60 | 3exp 1120 |
. . . . . . . 8
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (𝑤 ∈ 𝑧 → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))) |
62 | 39, 41, 61 | 3jaod 1429 |
. . . . . . 7
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ∨ 𝑤 ∈ 𝑧) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))) |
63 | 11, 62 | syl5 34 |
. . . . . 6
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((Ord 𝑧 ∧ Ord 𝑤) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))) |
64 | 63 | ex 416 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → ((Ord 𝑧 ∧ Ord 𝑤) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)))) |
65 | 10, 64 | mpdd 43 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))) |
66 | 65 | ralrimivv 3102 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)) |
67 | 2, 66 | sylan 583 |
. 2
⊢ ((𝐹:𝐴⟶𝐵 ∧ Smo 𝐹) → ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)) |
68 | | dff13 7018 |
. 2
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))) |
69 | 1, 67, 68 | sylanbrc 586 |
1
⊢ ((𝐹:𝐴⟶𝐵 ∧ Smo 𝐹) → 𝐹:𝐴–1-1→𝐵) |