Step | Hyp | Ref
| Expression |
1 | | fveq2 6668 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑞 → (𝐹‘𝑝) = (𝐹‘𝑞)) |
2 | 1 | ineq1d 4100 |
. . . . . . . . 9
⊢ (𝑝 = 𝑞 → ((𝐹‘𝑝) ∩ 𝐴) = ((𝐹‘𝑞) ∩ 𝐴)) |
3 | | sneq 4523 |
. . . . . . . . 9
⊢ (𝑝 = 𝑞 → {𝑝} = {𝑞}) |
4 | 2, 3 | eqeq12d 2754 |
. . . . . . . 8
⊢ (𝑝 = 𝑞 → (((𝐹‘𝑝) ∩ 𝐴) = {𝑝} ↔ ((𝐹‘𝑞) ∩ 𝐴) = {𝑞})) |
5 | 4 | cbvralvw 3348 |
. . . . . . 7
⊢
(∀𝑝 ∈
𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝} ↔ ∀𝑞 ∈ 𝐴 ((𝐹‘𝑞) ∩ 𝐴) = {𝑞}) |
6 | 5 | biimpi 219 |
. . . . . 6
⊢
(∀𝑝 ∈
𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝} → ∀𝑞 ∈ 𝐴 ((𝐹‘𝑞) ∩ 𝐴) = {𝑞}) |
7 | | ax-5 1916 |
. . . . . . . 8
⊢
(∀𝑝 ∈
𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝} → ∀𝑞∀𝑝 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝}) |
8 | | alral 3069 |
. . . . . . . 8
⊢
(∀𝑞∀𝑝 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝} → ∀𝑞 ∈ 𝐴 ∀𝑝 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝}) |
9 | | ralcom 3257 |
. . . . . . . . 9
⊢
(∀𝑞 ∈
𝐴 ∀𝑝 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝} ↔ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝}) |
10 | 9 | biimpi 219 |
. . . . . . . 8
⊢
(∀𝑞 ∈
𝐴 ∀𝑝 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝} → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝}) |
11 | 7, 8, 10 | 3syl 18 |
. . . . . . 7
⊢
(∀𝑝 ∈
𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝} → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝}) |
12 | | ax-5 1916 |
. . . . . . . 8
⊢
(∀𝑞 ∈
𝐴 ((𝐹‘𝑞) ∩ 𝐴) = {𝑞} → ∀𝑝∀𝑞 ∈ 𝐴 ((𝐹‘𝑞) ∩ 𝐴) = {𝑞}) |
13 | | alral 3069 |
. . . . . . . 8
⊢
(∀𝑝∀𝑞 ∈ 𝐴 ((𝐹‘𝑞) ∩ 𝐴) = {𝑞} → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((𝐹‘𝑞) ∩ 𝐴) = {𝑞}) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢
(∀𝑞 ∈
𝐴 ((𝐹‘𝑞) ∩ 𝐴) = {𝑞} → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((𝐹‘𝑞) ∩ 𝐴) = {𝑞}) |
15 | 11, 14 | anim12i 616 |
. . . . . 6
⊢
((∀𝑝 ∈
𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝} ∧ ∀𝑞 ∈ 𝐴 ((𝐹‘𝑞) ∩ 𝐴) = {𝑞}) → (∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝} ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((𝐹‘𝑞) ∩ 𝐴) = {𝑞})) |
16 | 6, 15 | mpdan 687 |
. . . . 5
⊢
(∀𝑝 ∈
𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝} → (∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝} ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((𝐹‘𝑞) ∩ 𝐴) = {𝑞})) |
17 | | r19.26-2 3085 |
. . . . 5
⊢
(∀𝑝 ∈
𝐴 ∀𝑞 ∈ 𝐴 (((𝐹‘𝑝) ∩ 𝐴) = {𝑝} ∧ ((𝐹‘𝑞) ∩ 𝐴) = {𝑞}) ↔ (∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝} ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((𝐹‘𝑞) ∩ 𝐴) = {𝑞})) |
18 | 16, 17 | sylibr 237 |
. . . 4
⊢
(∀𝑝 ∈
𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝} → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 (((𝐹‘𝑝) ∩ 𝐴) = {𝑝} ∧ ((𝐹‘𝑞) ∩ 𝐴) = {𝑞})) |
19 | | ineq1 4094 |
. . . . . . 7
⊢ ((𝐹‘𝑝) = (𝐹‘𝑞) → ((𝐹‘𝑝) ∩ 𝐴) = ((𝐹‘𝑞) ∩ 𝐴)) |
20 | | eqeq1 2742 |
. . . . . . . . 9
⊢ (((𝐹‘𝑝) ∩ 𝐴) = {𝑝} → (((𝐹‘𝑝) ∩ 𝐴) = ((𝐹‘𝑞) ∩ 𝐴) ↔ {𝑝} = ((𝐹‘𝑞) ∩ 𝐴))) |
21 | | eqcom 2745 |
. . . . . . . . 9
⊢ ({𝑝} = ((𝐹‘𝑞) ∩ 𝐴) ↔ ((𝐹‘𝑞) ∩ 𝐴) = {𝑝}) |
22 | 20, 21 | bitrdi 290 |
. . . . . . . 8
⊢ (((𝐹‘𝑝) ∩ 𝐴) = {𝑝} → (((𝐹‘𝑝) ∩ 𝐴) = ((𝐹‘𝑞) ∩ 𝐴) ↔ ((𝐹‘𝑞) ∩ 𝐴) = {𝑝})) |
23 | | eqeq1 2742 |
. . . . . . . . 9
⊢ (((𝐹‘𝑞) ∩ 𝐴) = {𝑞} → (((𝐹‘𝑞) ∩ 𝐴) = {𝑝} ↔ {𝑞} = {𝑝})) |
24 | | eqcom 2745 |
. . . . . . . . . 10
⊢ ({𝑞} = {𝑝} ↔ {𝑝} = {𝑞}) |
25 | | vex 3401 |
. . . . . . . . . . 11
⊢ 𝑝 ∈ V |
26 | | sneqbg 4726 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ V → ({𝑝} = {𝑞} ↔ 𝑝 = 𝑞)) |
27 | 25, 26 | ax-mp 5 |
. . . . . . . . . 10
⊢ ({𝑝} = {𝑞} ↔ 𝑝 = 𝑞) |
28 | 24, 27 | bitri 278 |
. . . . . . . . 9
⊢ ({𝑞} = {𝑝} ↔ 𝑝 = 𝑞) |
29 | 23, 28 | bitrdi 290 |
. . . . . . . 8
⊢ (((𝐹‘𝑞) ∩ 𝐴) = {𝑞} → (((𝐹‘𝑞) ∩ 𝐴) = {𝑝} ↔ 𝑝 = 𝑞)) |
30 | 22, 29 | sylan9bb 513 |
. . . . . . 7
⊢ ((((𝐹‘𝑝) ∩ 𝐴) = {𝑝} ∧ ((𝐹‘𝑞) ∩ 𝐴) = {𝑞}) → (((𝐹‘𝑝) ∩ 𝐴) = ((𝐹‘𝑞) ∩ 𝐴) ↔ 𝑝 = 𝑞)) |
31 | 19, 30 | syl5ib 247 |
. . . . . 6
⊢ ((((𝐹‘𝑝) ∩ 𝐴) = {𝑝} ∧ ((𝐹‘𝑞) ∩ 𝐴) = {𝑞}) → ((𝐹‘𝑝) = (𝐹‘𝑞) → 𝑝 = 𝑞)) |
32 | 31 | ralimi 3075 |
. . . . 5
⊢
(∀𝑞 ∈
𝐴 (((𝐹‘𝑝) ∩ 𝐴) = {𝑝} ∧ ((𝐹‘𝑞) ∩ 𝐴) = {𝑞}) → ∀𝑞 ∈ 𝐴 ((𝐹‘𝑝) = (𝐹‘𝑞) → 𝑝 = 𝑞)) |
33 | 32 | ralimi 3075 |
. . . 4
⊢
(∀𝑝 ∈
𝐴 ∀𝑞 ∈ 𝐴 (((𝐹‘𝑝) ∩ 𝐴) = {𝑝} ∧ ((𝐹‘𝑞) ∩ 𝐴) = {𝑞}) → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((𝐹‘𝑝) = (𝐹‘𝑞) → 𝑝 = 𝑞)) |
34 | 18, 33 | syl 17 |
. . 3
⊢
(∀𝑝 ∈
𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝} → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((𝐹‘𝑝) = (𝐹‘𝑞) → 𝑝 = 𝑞)) |
35 | 34 | anim2i 620 |
. 2
⊢ ((𝐹:𝐴⟶𝐽 ∧ ∀𝑝 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝}) → (𝐹:𝐴⟶𝐽 ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((𝐹‘𝑝) = (𝐹‘𝑞) → 𝑝 = 𝑞))) |
36 | | dff13 7018 |
. 2
⊢ (𝐹:𝐴–1-1→𝐽 ↔ (𝐹:𝐴⟶𝐽 ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ((𝐹‘𝑝) = (𝐹‘𝑞) → 𝑝 = 𝑞))) |
37 | 35, 36 | sylibr 237 |
1
⊢ ((𝐹:𝐴⟶𝐽 ∧ ∀𝑝 ∈ 𝐴 ((𝐹‘𝑝) ∩ 𝐴) = {𝑝}) → 𝐹:𝐴–1-1→𝐽) |