Step | Hyp | Ref
| Expression |
1 | | r2al 3125 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
2 | | simpl 486 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
3 | 2 | anim1i 618 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥)) |
4 | 3 | imim1i 63 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
5 | 4 | expd 419 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) |
6 | 5 | 2alimi 1820 |
. . . . . . 7
⊢
(∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) |
7 | 1, 6 | sylbi 220 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) |
8 | | r2al 3125 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) |
9 | 7, 8 | sylibr 237 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
10 | | elequ1 2119 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (𝑦 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥)) |
11 | | fveq2 6739 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤)) |
12 | 11 | eqeq2d 2750 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑤 → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑤))) |
13 | 12 | notbid 321 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (¬ (𝐹‘𝑥) = (𝐹‘𝑦) ↔ ¬ (𝐹‘𝑥) = (𝐹‘𝑤))) |
14 | 10, 13 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → ((𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)))) |
15 | 14 | cbvralvw 3373 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤))) |
16 | 15 | ralbii 3091 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤))) |
17 | | elequ2 2127 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧)) |
18 | | fveqeq2 6748 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) = (𝐹‘𝑤) ↔ (𝐹‘𝑧) = (𝐹‘𝑤))) |
19 | 18 | notbid 321 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (¬ (𝐹‘𝑥) = (𝐹‘𝑤) ↔ ¬ (𝐹‘𝑧) = (𝐹‘𝑤))) |
20 | 17, 19 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)) ↔ (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)))) |
21 | 20 | ralbidv 3121 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)))) |
22 | 21 | cbvralvw 3373 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑤)) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤))) |
23 | | elequ1 2119 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧)) |
24 | | fveq2 6739 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥)) |
25 | 24 | eqeq2d 2750 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑥 → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ (𝐹‘𝑧) = (𝐹‘𝑥))) |
26 | 25 | notbid 321 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑥 → (¬ (𝐹‘𝑧) = (𝐹‘𝑤) ↔ ¬ (𝐹‘𝑧) = (𝐹‘𝑥))) |
27 | 23, 26 | imbi12d 348 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → ((𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)))) |
28 | 27 | cbvralvw 3373 |
. . . . . . . . . . 11
⊢
(∀𝑤 ∈
𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥))) |
29 | 28 | ralbii 3091 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ ∀𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥))) |
30 | | elequ2 2127 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝑦)) |
31 | | fveqeq2 6748 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → ((𝐹‘𝑧) = (𝐹‘𝑥) ↔ (𝐹‘𝑦) = (𝐹‘𝑥))) |
32 | 31 | notbid 321 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑦 → (¬ (𝐹‘𝑧) = (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑦) = (𝐹‘𝑥))) |
33 | 30, 32 | imbi12d 348 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → ((𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))) |
34 | 33 | ralbidv 3121 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → (∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)))) |
35 | 34 | cbvralvw 3373 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑥)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥))) |
36 | 29, 35 | bitri 278 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑤 ∈ 𝑧 → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥))) |
37 | 16, 22, 36 | 3bitri 300 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥))) |
38 | | ralcom 3282 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥))) |
39 | 38 | biimpi 219 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝐴 ∀𝑥 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥))) |
40 | 37, 39 | sylbi 220 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥))) |
41 | 40 | ancri 553 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) |
42 | | r19.26-2 3096 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) |
43 | 41, 42 | sylibr 237 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) |
44 | 9, 43 | syl 17 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) |
45 | | fvres 6758 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
46 | | fvres 6758 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) |
47 | 45, 46 | eqeqan12d 2753 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑦))) |
48 | 47 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ On ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) ↔ (𝐹‘𝑥) = (𝐹‘𝑦))) |
49 | | ssel 3910 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → 𝑥 ∈ On)) |
50 | | ssel 3910 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → 𝑦 ∈ On)) |
51 | 49, 50 | anim12d 612 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ On → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ On ∧ 𝑦 ∈ On))) |
52 | | pm3.48 964 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → (¬ (𝐹‘𝑦) = (𝐹‘𝑥) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) |
53 | | oridm 905 |
. . . . . . . . . . . . . . 15
⊢ ((¬
(𝐹‘𝑥) = (𝐹‘𝑦) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) |
54 | | eqcom 2746 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = (𝐹‘𝑥)) |
55 | 54 | notbii 323 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝐹‘𝑥) = (𝐹‘𝑦) ↔ ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) |
56 | 55 | orbi1i 914 |
. . . . . . . . . . . . . . 15
⊢ ((¬
(𝐹‘𝑥) = (𝐹‘𝑦) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ (¬ (𝐹‘𝑦) = (𝐹‘𝑥) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
57 | 53, 56 | bitr3i 280 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝐹‘𝑥) = (𝐹‘𝑦) ↔ (¬ (𝐹‘𝑦) = (𝐹‘𝑥) ∨ ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
58 | 52, 57 | syl6ibr 255 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
59 | 58 | con2d 136 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥))) |
60 | | eloni 6244 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ On → Ord 𝑥) |
61 | | eloni 6244 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ On → Ord 𝑦) |
62 | | ordtri3 6270 |
. . . . . . . . . . . . . 14
⊢ ((Ord
𝑥 ∧ Ord 𝑦) → (𝑥 = 𝑦 ↔ ¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥))) |
63 | 62 | biimprd 251 |
. . . . . . . . . . . . 13
⊢ ((Ord
𝑥 ∧ Ord 𝑦) → (¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → 𝑥 = 𝑦)) |
64 | 60, 61, 63 | syl2an 599 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (¬ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥) → 𝑥 = 𝑦)) |
65 | 59, 64 | syl9r 78 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
66 | 51, 65 | syl6 35 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ On → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))) |
67 | 66 | imp32 422 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ On ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
68 | 48, 67 | sylbid 243 |
. . . . . . . 8
⊢ ((𝐴 ⊆ On ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) |
69 | 68 | exp32 424 |
. . . . . . 7
⊢ (𝐴 ⊆ On → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))) |
70 | 69 | a2d 29 |
. . . . . 6
⊢ (𝐴 ⊆ On → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))) |
71 | 70 | 2alimdv 1926 |
. . . . 5
⊢ (𝐴 ⊆ On →
(∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦)))) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)))) |
72 | | r2al 3125 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))))) |
73 | | r2al 3125 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))) |
74 | 71, 72, 73 | 3imtr4g 299 |
. . . 4
⊢ (𝐴 ⊆ On →
(∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 → ¬ (𝐹‘𝑦) = (𝐹‘𝑥)) ∧ (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))) |
75 | 44, 74 | syl5 34 |
. . 3
⊢ (𝐴 ⊆ On →
(∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))) |
76 | 75 | imdistani 572 |
. 2
⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → (𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))) |
77 | | tz7.48.1 |
. . . 4
⊢ 𝐹 Fn On |
78 | | fnssres 6522 |
. . . 4
⊢ ((𝐹 Fn On ∧ 𝐴 ⊆ On) → (𝐹 ↾ 𝐴) Fn 𝐴) |
79 | 77, 78 | mpan 690 |
. . 3
⊢ (𝐴 ⊆ On → (𝐹 ↾ 𝐴) Fn 𝐴) |
80 | | dffn2 6569 |
. . . 4
⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ (𝐹 ↾ 𝐴):𝐴⟶V) |
81 | | dff13 7089 |
. . . . . 6
⊢ ((𝐹 ↾ 𝐴):𝐴–1-1→V ↔ ((𝐹 ↾ 𝐴):𝐴⟶V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦))) |
82 | | df-f1 6406 |
. . . . . 6
⊢ ((𝐹 ↾ 𝐴):𝐴–1-1→V ↔ ((𝐹 ↾ 𝐴):𝐴⟶V ∧ Fun ◡(𝐹 ↾ 𝐴))) |
83 | 81, 82 | bitr3i 280 |
. . . . 5
⊢ (((𝐹 ↾ 𝐴):𝐴⟶V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) ↔ ((𝐹 ↾ 𝐴):𝐴⟶V ∧ Fun ◡(𝐹 ↾ 𝐴))) |
84 | 83 | simprbi 500 |
. . . 4
⊢ (((𝐹 ↾ 𝐴):𝐴⟶V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun ◡(𝐹 ↾ 𝐴)) |
85 | 80, 84 | sylanb 584 |
. . 3
⊢ (((𝐹 ↾ 𝐴) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun ◡(𝐹 ↾ 𝐴)) |
86 | 79, 85 | sylan 583 |
. 2
⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (((𝐹 ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑦) → 𝑥 = 𝑦)) → Fun ◡(𝐹 ↾ 𝐴)) |
87 | 76, 86 | syl 17 |
1
⊢ ((𝐴 ⊆ On ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → Fun ◡(𝐹 ↾ 𝐴)) |