Step | Hyp | Ref
| Expression |
1 | | elpri 4589 |
. . . . . . 7
⊢ (𝑥 ∈ {∅, 𝐴} → (𝑥 = ∅ ∨ 𝑥 = 𝐴)) |
2 | | topontop 21521 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
3 | 2 | ad2antrr 724 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → 𝐽 ∈ Top) |
4 | | 0opn 21512 |
. . . . . . . . . 10
⊢ (𝐽 ∈ Top → ∅
∈ 𝐽) |
5 | 3, 4 | syl 17 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → ∅ ∈ 𝐽) |
6 | | imaeq2 5925 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (◡𝑓 “ 𝑥) = (◡𝑓 “ ∅)) |
7 | | ima0 5945 |
. . . . . . . . . . 11
⊢ (◡𝑓 “ ∅) = ∅ |
8 | 6, 7 | syl6eq 2872 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → (◡𝑓 “ 𝑥) = ∅) |
9 | 8 | eleq1d 2897 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → ((◡𝑓 “ 𝑥) ∈ 𝐽 ↔ ∅ ∈ 𝐽)) |
10 | 5, 9 | syl5ibrcom 249 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → (𝑥 = ∅ → (◡𝑓 “ 𝑥) ∈ 𝐽)) |
11 | | fimacnv 6839 |
. . . . . . . . . . 11
⊢ (𝑓:𝑋⟶𝐴 → (◡𝑓 “ 𝐴) = 𝑋) |
12 | 11 | adantl 484 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → (◡𝑓 “ 𝐴) = 𝑋) |
13 | | toponmax 21534 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
14 | 13 | ad2antrr 724 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → 𝑋 ∈ 𝐽) |
15 | 12, 14 | eqeltrd 2913 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → (◡𝑓 “ 𝐴) ∈ 𝐽) |
16 | | imaeq2 5925 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (◡𝑓 “ 𝑥) = (◡𝑓 “ 𝐴)) |
17 | 16 | eleq1d 2897 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((◡𝑓 “ 𝑥) ∈ 𝐽 ↔ (◡𝑓 “ 𝐴) ∈ 𝐽)) |
18 | 15, 17 | syl5ibrcom 249 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → (𝑥 = 𝐴 → (◡𝑓 “ 𝑥) ∈ 𝐽)) |
19 | 10, 18 | jaod 855 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) → (◡𝑓 “ 𝑥) ∈ 𝐽)) |
20 | 1, 19 | syl5 34 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → (𝑥 ∈ {∅, 𝐴} → (◡𝑓 “ 𝑥) ∈ 𝐽)) |
21 | 20 | ralrimiv 3181 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → ∀𝑥 ∈ {∅, 𝐴} (◡𝑓 “ 𝑥) ∈ 𝐽) |
22 | 21 | ex 415 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝑓:𝑋⟶𝐴 → ∀𝑥 ∈ {∅, 𝐴} (◡𝑓 “ 𝑥) ∈ 𝐽)) |
23 | 22 | pm4.71d 564 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝑓:𝑋⟶𝐴 ↔ (𝑓:𝑋⟶𝐴 ∧ ∀𝑥 ∈ {∅, 𝐴} (◡𝑓 “ 𝑥) ∈ 𝐽))) |
24 | | id 22 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉) |
25 | | elmapg 8419 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐽) → (𝑓 ∈ (𝐴 ↑m 𝑋) ↔ 𝑓:𝑋⟶𝐴)) |
26 | 24, 13, 25 | syl2anr 598 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝑓 ∈ (𝐴 ↑m 𝑋) ↔ 𝑓:𝑋⟶𝐴)) |
27 | | indistopon 21609 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → {∅, 𝐴} ∈ (TopOn‘𝐴)) |
28 | | iscn 21843 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {∅, 𝐴} ∈ (TopOn‘𝐴)) → (𝑓 ∈ (𝐽 Cn {∅, 𝐴}) ↔ (𝑓:𝑋⟶𝐴 ∧ ∀𝑥 ∈ {∅, 𝐴} (◡𝑓 “ 𝑥) ∈ 𝐽))) |
29 | 27, 28 | sylan2 594 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝑓 ∈ (𝐽 Cn {∅, 𝐴}) ↔ (𝑓:𝑋⟶𝐴 ∧ ∀𝑥 ∈ {∅, 𝐴} (◡𝑓 “ 𝑥) ∈ 𝐽))) |
30 | 23, 26, 29 | 3bitr4rd 314 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝑓 ∈ (𝐽 Cn {∅, 𝐴}) ↔ 𝑓 ∈ (𝐴 ↑m 𝑋))) |
31 | 30 | eqrdv 2819 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐽 Cn {∅, 𝐴}) = (𝐴 ↑m 𝑋)) |