Step | Hyp | Ref
| Expression |
1 | | ssid 3624 |
. . 3
⊢ On
⊆ On |
2 | | onelon 5748 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
3 | 2 | ancoms 469 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ On) → 𝑦 ∈ On) |
4 | | tz7.48.1 |
. . . . . . . . . . 11
⊢ 𝐹 Fn On |
5 | | fndm 5990 |
. . . . . . . . . . 11
⊢ (𝐹 Fn On → dom 𝐹 = On) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . . 10
⊢ dom 𝐹 = On |
7 | 6 | eleq2i 2693 |
. . . . . . . . 9
⊢ (𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ On) |
8 | | fnfun 5988 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn On → Fun 𝐹) |
9 | 4, 8 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ Fun 𝐹 |
10 | | funfvima 6492 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝑦 ∈ 𝑥 → (𝐹‘𝑦) ∈ (𝐹 “ 𝑥))) |
11 | 9, 10 | mpan 706 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ dom 𝐹 → (𝑦 ∈ 𝑥 → (𝐹‘𝑦) ∈ (𝐹 “ 𝑥))) |
12 | 11 | impcom 446 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) ∈ (𝐹 “ 𝑥)) |
13 | | eleq1a 2696 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑦) ∈ (𝐹 “ 𝑥) → ((𝐹‘𝑥) = (𝐹‘𝑦) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑥))) |
14 | | eldifn 3733 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ¬ (𝐹‘𝑥) ∈ (𝐹 “ 𝑥)) |
15 | 13, 14 | nsyli 155 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑦) ∈ (𝐹 “ 𝑥) → ((𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
16 | 12, 15 | syl 17 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ dom 𝐹) → ((𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
17 | 7, 16 | sylan2br 493 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ On) → ((𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
18 | 3, 17 | syldan 487 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ On) → ((𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
19 | 18 | expimpd 629 |
. . . . . 6
⊢ (𝑦 ∈ 𝑥 → ((𝑥 ∈ On ∧ (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))) → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
20 | 19 | com12 32 |
. . . . 5
⊢ ((𝑥 ∈ On ∧ (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))) → (𝑦 ∈ 𝑥 → ¬ (𝐹‘𝑥) = (𝐹‘𝑦))) |
21 | 20 | ralrimiv 2965 |
. . . 4
⊢ ((𝑥 ∈ On ∧ (𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥))) → ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) |
22 | 21 | ralimiaa 2951 |
. . 3
⊢
(∀𝑥 ∈ On
(𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → ∀𝑥 ∈ On ∀𝑦 ∈ 𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) |
23 | 4 | tz7.48lem 7536 |
. . 3
⊢ ((On
⊆ On ∧ ∀𝑥
∈ On ∀𝑦 ∈
𝑥 ¬ (𝐹‘𝑥) = (𝐹‘𝑦)) → Fun ◡(𝐹 ↾ On)) |
24 | 1, 22, 23 | sylancr 695 |
. 2
⊢
(∀𝑥 ∈ On
(𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → Fun ◡(𝐹 ↾ On)) |
25 | | fnrel 5989 |
. . . . . 6
⊢ (𝐹 Fn On → Rel 𝐹) |
26 | 4, 25 | ax-mp 5 |
. . . . 5
⊢ Rel 𝐹 |
27 | 6 | eqimssi 3659 |
. . . . 5
⊢ dom 𝐹 ⊆ On |
28 | | relssres 5437 |
. . . . 5
⊢ ((Rel
𝐹 ∧ dom 𝐹 ⊆ On) → (𝐹 ↾ On) = 𝐹) |
29 | 26, 27, 28 | mp2an 708 |
. . . 4
⊢ (𝐹 ↾ On) = 𝐹 |
30 | 29 | cnveqi 5297 |
. . 3
⊢ ◡(𝐹 ↾ On) = ◡𝐹 |
31 | 30 | funeqi 5909 |
. 2
⊢ (Fun
◡(𝐹 ↾ On) ↔ Fun ◡𝐹) |
32 | 24, 31 | sylib 208 |
1
⊢
(∀𝑥 ∈ On
(𝐹‘𝑥) ∈ (𝐴 ∖ (𝐹 “ 𝑥)) → Fun ◡𝐹) |