Step | Hyp | Ref
| Expression |
1 | | simplrl 525 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ({𝐴} ∈ 𝐽 ∧ 𝑓:𝑋⟶𝑌)) ∧ (𝑥 ∈ 𝐾 ∧ (𝑓‘𝐴) ∈ 𝑥)) → {𝐴} ∈ 𝐽) |
2 | | simpll3 1028 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ({𝐴} ∈ 𝐽 ∧ 𝑓:𝑋⟶𝑌)) ∧ (𝑥 ∈ 𝐾 ∧ (𝑓‘𝐴) ∈ 𝑥)) → 𝐴 ∈ 𝑋) |
3 | | snidg 3604 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ {𝐴}) |
4 | 2, 3 | syl 14 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ({𝐴} ∈ 𝐽 ∧ 𝑓:𝑋⟶𝑌)) ∧ (𝑥 ∈ 𝐾 ∧ (𝑓‘𝐴) ∈ 𝑥)) → 𝐴 ∈ {𝐴}) |
5 | | simprr 522 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ({𝐴} ∈ 𝐽 ∧ 𝑓:𝑋⟶𝑌)) ∧ (𝑥 ∈ 𝐾 ∧ (𝑓‘𝐴) ∈ 𝑥)) → (𝑓‘𝐴) ∈ 𝑥) |
6 | | simplrr 526 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ({𝐴} ∈ 𝐽 ∧ 𝑓:𝑋⟶𝑌)) ∧ (𝑥 ∈ 𝐾 ∧ (𝑓‘𝐴) ∈ 𝑥)) → 𝑓:𝑋⟶𝑌) |
7 | | ffn 5336 |
. . . . . . . . . . 11
⊢ (𝑓:𝑋⟶𝑌 → 𝑓 Fn 𝑋) |
8 | | elpreima 5603 |
. . . . . . . . . . 11
⊢ (𝑓 Fn 𝑋 → (𝐴 ∈ (◡𝑓 “ 𝑥) ↔ (𝐴 ∈ 𝑋 ∧ (𝑓‘𝐴) ∈ 𝑥))) |
9 | 6, 7, 8 | 3syl 17 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ({𝐴} ∈ 𝐽 ∧ 𝑓:𝑋⟶𝑌)) ∧ (𝑥 ∈ 𝐾 ∧ (𝑓‘𝐴) ∈ 𝑥)) → (𝐴 ∈ (◡𝑓 “ 𝑥) ↔ (𝐴 ∈ 𝑋 ∧ (𝑓‘𝐴) ∈ 𝑥))) |
10 | 2, 5, 9 | mpbir2and 934 |
. . . . . . . . 9
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ({𝐴} ∈ 𝐽 ∧ 𝑓:𝑋⟶𝑌)) ∧ (𝑥 ∈ 𝐾 ∧ (𝑓‘𝐴) ∈ 𝑥)) → 𝐴 ∈ (◡𝑓 “ 𝑥)) |
11 | 10 | snssd 3717 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ({𝐴} ∈ 𝐽 ∧ 𝑓:𝑋⟶𝑌)) ∧ (𝑥 ∈ 𝐾 ∧ (𝑓‘𝐴) ∈ 𝑥)) → {𝐴} ⊆ (◡𝑓 “ 𝑥)) |
12 | | eleq2 2229 |
. . . . . . . . . 10
⊢ (𝑦 = {𝐴} → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ {𝐴})) |
13 | | sseq1 3164 |
. . . . . . . . . 10
⊢ (𝑦 = {𝐴} → (𝑦 ⊆ (◡𝑓 “ 𝑥) ↔ {𝐴} ⊆ (◡𝑓 “ 𝑥))) |
14 | 12, 13 | anbi12d 465 |
. . . . . . . . 9
⊢ (𝑦 = {𝐴} → ((𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ (◡𝑓 “ 𝑥)) ↔ (𝐴 ∈ {𝐴} ∧ {𝐴} ⊆ (◡𝑓 “ 𝑥)))) |
15 | 14 | rspcev 2829 |
. . . . . . . 8
⊢ (({𝐴} ∈ 𝐽 ∧ (𝐴 ∈ {𝐴} ∧ {𝐴} ⊆ (◡𝑓 “ 𝑥))) → ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ (◡𝑓 “ 𝑥))) |
16 | 1, 4, 11, 15 | syl12anc 1226 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ({𝐴} ∈ 𝐽 ∧ 𝑓:𝑋⟶𝑌)) ∧ (𝑥 ∈ 𝐾 ∧ (𝑓‘𝐴) ∈ 𝑥)) → ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ (◡𝑓 “ 𝑥))) |
17 | 16 | expr 373 |
. . . . . 6
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ({𝐴} ∈ 𝐽 ∧ 𝑓:𝑋⟶𝑌)) ∧ 𝑥 ∈ 𝐾) → ((𝑓‘𝐴) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ (◡𝑓 “ 𝑥)))) |
18 | 17 | ralrimiva 2538 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ ({𝐴} ∈ 𝐽 ∧ 𝑓:𝑋⟶𝑌)) → ∀𝑥 ∈ 𝐾 ((𝑓‘𝐴) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ (◡𝑓 “ 𝑥)))) |
19 | 18 | expr 373 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ {𝐴} ∈ 𝐽) → (𝑓:𝑋⟶𝑌 → ∀𝑥 ∈ 𝐾 ((𝑓‘𝐴) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ (◡𝑓 “ 𝑥))))) |
20 | 19 | pm4.71d 391 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ {𝐴} ∈ 𝐽) → (𝑓:𝑋⟶𝑌 ↔ (𝑓:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 ((𝑓‘𝐴) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ (◡𝑓 “ 𝑥)))))) |
21 | | simpl2 991 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ {𝐴} ∈ 𝐽) → 𝐾 ∈ (TopOn‘𝑌)) |
22 | | toponmax 12623 |
. . . . 5
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾) |
23 | 21, 22 | syl 14 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ {𝐴} ∈ 𝐽) → 𝑌 ∈ 𝐾) |
24 | | simpl1 990 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ {𝐴} ∈ 𝐽) → 𝐽 ∈ (TopOn‘𝑋)) |
25 | | toponmax 12623 |
. . . . 5
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
26 | 24, 25 | syl 14 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ {𝐴} ∈ 𝐽) → 𝑋 ∈ 𝐽) |
27 | 23, 26 | elmapd 6624 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ {𝐴} ∈ 𝐽) → (𝑓 ∈ (𝑌 ↑𝑚 𝑋) ↔ 𝑓:𝑋⟶𝑌)) |
28 | | iscnp3 12803 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝑓 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝑓:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 ((𝑓‘𝐴) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ (◡𝑓 “ 𝑥)))))) |
29 | 28 | adantr 274 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ {𝐴} ∈ 𝐽) → (𝑓 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝑓:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 ((𝑓‘𝐴) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ (◡𝑓 “ 𝑥)))))) |
30 | 20, 27, 29 | 3bitr4rd 220 |
. 2
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ {𝐴} ∈ 𝐽) → (𝑓 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ 𝑓 ∈ (𝑌 ↑𝑚 𝑋))) |
31 | 30 | eqrdv 2163 |
1
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) ∧ {𝐴} ∈ 𝐽) → ((𝐽 CnP 𝐾)‘𝐴) = (𝑌 ↑𝑚 𝑋)) |