| Step | Hyp | Ref
| Expression |
| 1 | | kqval.2 |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) |
| 2 | 1 | kqffn 23733 |
. . . 4
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋) |
| 3 | 2 | 3ad2ant1 1134 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) → 𝐹 Fn 𝑋) |
| 4 | | toponss 22933 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → 𝑈 ⊆ 𝑋) |
| 5 | 4 | 3adant3 1133 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) → 𝑈 ⊆ 𝑋) |
| 6 | | fnfvima 7253 |
. . . 4
⊢ ((𝐹 Fn 𝑋 ∧ 𝑈 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑈) → (𝐹‘𝐴) ∈ (𝐹 “ 𝑈)) |
| 7 | 6 | 3expia 1122 |
. . 3
⊢ ((𝐹 Fn 𝑋 ∧ 𝑈 ⊆ 𝑋) → (𝐴 ∈ 𝑈 → (𝐹‘𝐴) ∈ (𝐹 “ 𝑈))) |
| 8 | 3, 5, 7 | syl2anc 584 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ 𝑈 → (𝐹‘𝐴) ∈ (𝐹 “ 𝑈))) |
| 9 | | fnfun 6668 |
. . . 4
⊢ (𝐹 Fn 𝑋 → Fun 𝐹) |
| 10 | | fvelima 6974 |
. . . . 5
⊢ ((Fun
𝐹 ∧ (𝐹‘𝐴) ∈ (𝐹 “ 𝑈)) → ∃𝑧 ∈ 𝑈 (𝐹‘𝑧) = (𝐹‘𝐴)) |
| 11 | 10 | ex 412 |
. . . 4
⊢ (Fun
𝐹 → ((𝐹‘𝐴) ∈ (𝐹 “ 𝑈) → ∃𝑧 ∈ 𝑈 (𝐹‘𝑧) = (𝐹‘𝐴))) |
| 12 | 3, 9, 11 | 3syl 18 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴) ∈ (𝐹 “ 𝑈) → ∃𝑧 ∈ 𝑈 (𝐹‘𝑧) = (𝐹‘𝐴))) |
| 13 | | simpl1 1192 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) ∧ 𝑧 ∈ 𝑈) → 𝐽 ∈ (TopOn‘𝑋)) |
| 14 | 5 | sselda 3983 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ 𝑋) |
| 15 | | simpl3 1194 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) ∧ 𝑧 ∈ 𝑈) → 𝐴 ∈ 𝑋) |
| 16 | 1 | kqfeq 23732 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝑧) = (𝐹‘𝐴) ↔ ∀𝑦 ∈ 𝐽 (𝑧 ∈ 𝑦 ↔ 𝐴 ∈ 𝑦))) |
| 17 | 13, 14, 15, 16 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) ∧ 𝑧 ∈ 𝑈) → ((𝐹‘𝑧) = (𝐹‘𝐴) ↔ ∀𝑦 ∈ 𝐽 (𝑧 ∈ 𝑦 ↔ 𝐴 ∈ 𝑦))) |
| 18 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑦 = 𝑤 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑤)) |
| 19 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑦 = 𝑤 → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑤)) |
| 20 | 18, 19 | bibi12d 345 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → ((𝑧 ∈ 𝑦 ↔ 𝐴 ∈ 𝑦) ↔ (𝑧 ∈ 𝑤 ↔ 𝐴 ∈ 𝑤))) |
| 21 | 20 | cbvralvw 3237 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝐽 (𝑧 ∈ 𝑦 ↔ 𝐴 ∈ 𝑦) ↔ ∀𝑤 ∈ 𝐽 (𝑧 ∈ 𝑤 ↔ 𝐴 ∈ 𝑤)) |
| 22 | 17, 21 | bitrdi 287 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) ∧ 𝑧 ∈ 𝑈) → ((𝐹‘𝑧) = (𝐹‘𝐴) ↔ ∀𝑤 ∈ 𝐽 (𝑧 ∈ 𝑤 ↔ 𝐴 ∈ 𝑤))) |
| 23 | | simpl2 1193 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) ∧ 𝑧 ∈ 𝑈) → 𝑈 ∈ 𝐽) |
| 24 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑤 = 𝑈 → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑈)) |
| 25 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑤 = 𝑈 → (𝐴 ∈ 𝑤 ↔ 𝐴 ∈ 𝑈)) |
| 26 | 24, 25 | bibi12d 345 |
. . . . . . . 8
⊢ (𝑤 = 𝑈 → ((𝑧 ∈ 𝑤 ↔ 𝐴 ∈ 𝑤) ↔ (𝑧 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈))) |
| 27 | 26 | rspcv 3618 |
. . . . . . 7
⊢ (𝑈 ∈ 𝐽 → (∀𝑤 ∈ 𝐽 (𝑧 ∈ 𝑤 ↔ 𝐴 ∈ 𝑤) → (𝑧 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈))) |
| 28 | 23, 27 | syl 17 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) ∧ 𝑧 ∈ 𝑈) → (∀𝑤 ∈ 𝐽 (𝑧 ∈ 𝑤 ↔ 𝐴 ∈ 𝑤) → (𝑧 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈))) |
| 29 | 22, 28 | sylbid 240 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) ∧ 𝑧 ∈ 𝑈) → ((𝐹‘𝑧) = (𝐹‘𝐴) → (𝑧 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈))) |
| 30 | | simpr 484 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ 𝑈) |
| 31 | | biimp 215 |
. . . . 5
⊢ ((𝑧 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈) → (𝑧 ∈ 𝑈 → 𝐴 ∈ 𝑈)) |
| 32 | 29, 30, 31 | syl6ci 71 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) ∧ 𝑧 ∈ 𝑈) → ((𝐹‘𝑧) = (𝐹‘𝐴) → 𝐴 ∈ 𝑈)) |
| 33 | 32 | rexlimdva 3155 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) → (∃𝑧 ∈ 𝑈 (𝐹‘𝑧) = (𝐹‘𝐴) → 𝐴 ∈ 𝑈)) |
| 34 | 12, 33 | syld 47 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴) ∈ (𝐹 “ 𝑈) → 𝐴 ∈ 𝑈)) |
| 35 | 8, 34 | impbid 212 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ 𝑈 ↔ (𝐹‘𝐴) ∈ (𝐹 “ 𝑈))) |