| Step | Hyp | Ref
| Expression |
| 1 | | elpri 4649 |
. . . . . . 7
⊢ (𝑥 ∈ {∅, 𝐴} → (𝑥 = ∅ ∨ 𝑥 = 𝐴)) |
| 2 | | topontop 22919 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
| 3 | 2 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → 𝐽 ∈ Top) |
| 4 | | 0opn 22910 |
. . . . . . . . . 10
⊢ (𝐽 ∈ Top → ∅
∈ 𝐽) |
| 5 | 3, 4 | syl 17 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → ∅ ∈ 𝐽) |
| 6 | | imaeq2 6074 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (◡𝑓 “ 𝑥) = (◡𝑓 “ ∅)) |
| 7 | | ima0 6095 |
. . . . . . . . . . 11
⊢ (◡𝑓 “ ∅) = ∅ |
| 8 | 6, 7 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → (◡𝑓 “ 𝑥) = ∅) |
| 9 | 8 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → ((◡𝑓 “ 𝑥) ∈ 𝐽 ↔ ∅ ∈ 𝐽)) |
| 10 | 5, 9 | syl5ibrcom 247 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → (𝑥 = ∅ → (◡𝑓 “ 𝑥) ∈ 𝐽)) |
| 11 | | fimacnv 6758 |
. . . . . . . . . . 11
⊢ (𝑓:𝑋⟶𝐴 → (◡𝑓 “ 𝐴) = 𝑋) |
| 12 | 11 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → (◡𝑓 “ 𝐴) = 𝑋) |
| 13 | | toponmax 22932 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
| 14 | 13 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → 𝑋 ∈ 𝐽) |
| 15 | 12, 14 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → (◡𝑓 “ 𝐴) ∈ 𝐽) |
| 16 | | imaeq2 6074 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (◡𝑓 “ 𝑥) = (◡𝑓 “ 𝐴)) |
| 17 | 16 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((◡𝑓 “ 𝑥) ∈ 𝐽 ↔ (◡𝑓 “ 𝐴) ∈ 𝐽)) |
| 18 | 15, 17 | syl5ibrcom 247 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → (𝑥 = 𝐴 → (◡𝑓 “ 𝑥) ∈ 𝐽)) |
| 19 | 10, 18 | jaod 860 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) → (◡𝑓 “ 𝑥) ∈ 𝐽)) |
| 20 | 1, 19 | syl5 34 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → (𝑥 ∈ {∅, 𝐴} → (◡𝑓 “ 𝑥) ∈ 𝐽)) |
| 21 | 20 | ralrimiv 3145 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) ∧ 𝑓:𝑋⟶𝐴) → ∀𝑥 ∈ {∅, 𝐴} (◡𝑓 “ 𝑥) ∈ 𝐽) |
| 22 | 21 | ex 412 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝑓:𝑋⟶𝐴 → ∀𝑥 ∈ {∅, 𝐴} (◡𝑓 “ 𝑥) ∈ 𝐽)) |
| 23 | 22 | pm4.71d 561 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝑓:𝑋⟶𝐴 ↔ (𝑓:𝑋⟶𝐴 ∧ ∀𝑥 ∈ {∅, 𝐴} (◡𝑓 “ 𝑥) ∈ 𝐽))) |
| 24 | | id 22 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉) |
| 25 | | elmapg 8879 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐽) → (𝑓 ∈ (𝐴 ↑m 𝑋) ↔ 𝑓:𝑋⟶𝐴)) |
| 26 | 24, 13, 25 | syl2anr 597 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝑓 ∈ (𝐴 ↑m 𝑋) ↔ 𝑓:𝑋⟶𝐴)) |
| 27 | | indistopon 23008 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → {∅, 𝐴} ∈ (TopOn‘𝐴)) |
| 28 | | iscn 23243 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ {∅, 𝐴} ∈ (TopOn‘𝐴)) → (𝑓 ∈ (𝐽 Cn {∅, 𝐴}) ↔ (𝑓:𝑋⟶𝐴 ∧ ∀𝑥 ∈ {∅, 𝐴} (◡𝑓 “ 𝑥) ∈ 𝐽))) |
| 29 | 27, 28 | sylan2 593 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝑓 ∈ (𝐽 Cn {∅, 𝐴}) ↔ (𝑓:𝑋⟶𝐴 ∧ ∀𝑥 ∈ {∅, 𝐴} (◡𝑓 “ 𝑥) ∈ 𝐽))) |
| 30 | 23, 26, 29 | 3bitr4rd 312 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝑓 ∈ (𝐽 Cn {∅, 𝐴}) ↔ 𝑓 ∈ (𝐴 ↑m 𝑋))) |
| 31 | 30 | eqrdv 2735 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐽 Cn {∅, 𝐴}) = (𝐴 ↑m 𝑋)) |