Step | Hyp | Ref
| Expression |
1 | | txdis1cn.f |
. . 3
⊢ (𝜑 → 𝐹 Fn (𝑋 × 𝑌)) |
2 | | txdis1cn.j |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑌)) |
3 | 2 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑌)) |
4 | | txdis1cn.k |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ Top) |
5 | | eqid 2778 |
. . . . . . . . 9
⊢ ∪ 𝐾 =
∪ 𝐾 |
6 | 5 | toptopon 21133 |
. . . . . . . 8
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
7 | 4, 6 | sylib 210 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
8 | 7 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
9 | | txdis1cn.1 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) |
10 | | cnf2 21465 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)):𝑌⟶∪ 𝐾) |
11 | 3, 8, 9, 10 | syl3anc 1439 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)):𝑌⟶∪ 𝐾) |
12 | | eqid 2778 |
. . . . . 6
⊢ (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) = (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) |
13 | 12 | fmpt 6646 |
. . . . 5
⊢
(∀𝑦 ∈
𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾 ↔ (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)):𝑌⟶∪ 𝐾) |
14 | 11, 13 | sylibr 226 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾) |
15 | 14 | ralrimiva 3148 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾) |
16 | | ffnov 7043 |
. . 3
⊢ (𝐹:(𝑋 × 𝑌)⟶∪ 𝐾 ↔ (𝐹 Fn (𝑋 × 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾)) |
17 | 1, 15, 16 | sylanbrc 578 |
. 2
⊢ (𝜑 → 𝐹:(𝑋 × 𝑌)⟶∪ 𝐾) |
18 | | cnvimass 5741 |
. . . . . . . 8
⊢ (◡𝐹 “ 𝑢) ⊆ dom 𝐹 |
19 | 1 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → 𝐹 Fn (𝑋 × 𝑌)) |
20 | | fndm 6237 |
. . . . . . . . 9
⊢ (𝐹 Fn (𝑋 × 𝑌) → dom 𝐹 = (𝑋 × 𝑌)) |
21 | 19, 20 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → dom 𝐹 = (𝑋 × 𝑌)) |
22 | 18, 21 | syl5sseq 3872 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (◡𝐹 “ 𝑢) ⊆ (𝑋 × 𝑌)) |
23 | | relxp 5375 |
. . . . . . 7
⊢ Rel
(𝑋 × 𝑌) |
24 | | relss 5456 |
. . . . . . 7
⊢ ((◡𝐹 “ 𝑢) ⊆ (𝑋 × 𝑌) → (Rel (𝑋 × 𝑌) → Rel (◡𝐹 “ 𝑢))) |
25 | 22, 23, 24 | mpisyl 21 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → Rel (◡𝐹 “ 𝑢)) |
26 | | elpreima 6602 |
. . . . . . . 8
⊢ (𝐹 Fn (𝑋 × 𝑌) → (〈𝑥, 𝑧〉 ∈ (◡𝐹 “ 𝑢) ↔ (〈𝑥, 𝑧〉 ∈ (𝑋 × 𝑌) ∧ (𝐹‘〈𝑥, 𝑧〉) ∈ 𝑢))) |
27 | 19, 26 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑧〉 ∈ (◡𝐹 “ 𝑢) ↔ (〈𝑥, 𝑧〉 ∈ (𝑋 × 𝑌) ∧ (𝐹‘〈𝑥, 𝑧〉) ∈ 𝑢))) |
28 | | opelxp 5393 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑧〉 ∈ (𝑋 × 𝑌) ↔ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌)) |
29 | | df-ov 6927 |
. . . . . . . . . . 11
⊢ (𝑥𝐹𝑧) = (𝐹‘〈𝑥, 𝑧〉) |
30 | 29 | eqcomi 2787 |
. . . . . . . . . 10
⊢ (𝐹‘〈𝑥, 𝑧〉) = (𝑥𝐹𝑧) |
31 | 30 | eleq1i 2850 |
. . . . . . . . 9
⊢ ((𝐹‘〈𝑥, 𝑧〉) ∈ 𝑢 ↔ (𝑥𝐹𝑧) ∈ 𝑢) |
32 | 28, 31 | anbi12i 620 |
. . . . . . . 8
⊢
((〈𝑥, 𝑧〉 ∈ (𝑋 × 𝑌) ∧ (𝐹‘〈𝑥, 𝑧〉) ∈ 𝑢) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) |
33 | | simprll 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑥 ∈ 𝑋) |
34 | | snelpwi 5146 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋 → {𝑥} ∈ 𝒫 𝑋) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑥} ∈ 𝒫 𝑋) |
36 | 12 | mptpreima 5884 |
. . . . . . . . . . . 12
⊢ (◡(𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} |
37 | 9 | adantrr 707 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) |
38 | 37 | ad2ant2r 737 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) |
39 | | simplr 759 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑢 ∈ 𝐾) |
40 | | cnima 21481 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾) ∧ 𝑢 ∈ 𝐾) → (◡(𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) ∈ 𝐽) |
41 | 38, 39, 40 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (◡(𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) ∈ 𝐽) |
42 | 36, 41 | syl5eqelr 2864 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ∈ 𝐽) |
43 | | simprlr 770 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑧 ∈ 𝑌) |
44 | | simprr 763 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (𝑥𝐹𝑧) ∈ 𝑢) |
45 | | vsnid 4431 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ {𝑥} |
46 | | opelxp 5393 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑧〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑥 ∈ {𝑥} ∧ 𝑧 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) |
47 | 45, 46 | mpbiran 699 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑧〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ 𝑧 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) |
48 | | oveq2 6932 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → (𝑥𝐹𝑦) = (𝑥𝐹𝑧)) |
49 | 48 | eleq1d 2844 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → ((𝑥𝐹𝑦) ∈ 𝑢 ↔ (𝑥𝐹𝑧) ∈ 𝑢)) |
50 | 49 | elrab 3572 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ↔ (𝑧 ∈ 𝑌 ∧ (𝑥𝐹𝑧) ∈ 𝑢)) |
51 | 47, 50 | bitri 267 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑧〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑧 ∈ 𝑌 ∧ (𝑥𝐹𝑧) ∈ 𝑢)) |
52 | 43, 44, 51 | sylanbrc 578 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 〈𝑥, 𝑧〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) |
53 | | relxp 5375 |
. . . . . . . . . . . . 13
⊢ Rel
({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) |
54 | 53 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → Rel ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) |
55 | | opelxp 5393 |
. . . . . . . . . . . . 13
⊢
(〈𝑛, 𝑚〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) |
56 | 33 | snssd 4573 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑥} ⊆ 𝑋) |
57 | 56 | sselda 3821 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ 𝑛 ∈ {𝑥}) → 𝑛 ∈ 𝑋) |
58 | 57 | adantrr 707 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑛 ∈ 𝑋) |
59 | | elrabi 3567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → 𝑚 ∈ 𝑌) |
60 | 59 | ad2antll 719 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑚 ∈ 𝑌) |
61 | | opelxp 5393 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑛, 𝑚〉 ∈ (𝑋 × 𝑌) ↔ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑌)) |
62 | 58, 60, 61 | sylanbrc 578 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 〈𝑛, 𝑚〉 ∈ (𝑋 × 𝑌)) |
63 | | df-ov 6927 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛𝐹𝑚) = (𝐹‘〈𝑛, 𝑚〉) |
64 | | elsni 4415 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ {𝑥} → 𝑛 = 𝑥) |
65 | 64 | ad2antrl 718 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑛 = 𝑥) |
66 | 65 | oveq1d 6939 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝑛𝐹𝑚) = (𝑥𝐹𝑚)) |
67 | 63, 66 | syl5eqr 2828 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝐹‘〈𝑛, 𝑚〉) = (𝑥𝐹𝑚)) |
68 | | oveq2 6932 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑚 → (𝑥𝐹𝑦) = (𝑥𝐹𝑚)) |
69 | 68 | eleq1d 2844 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑚 → ((𝑥𝐹𝑦) ∈ 𝑢 ↔ (𝑥𝐹𝑚) ∈ 𝑢)) |
70 | 69 | elrab 3572 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ↔ (𝑚 ∈ 𝑌 ∧ (𝑥𝐹𝑚) ∈ 𝑢)) |
71 | 70 | simprbi 492 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (𝑥𝐹𝑚) ∈ 𝑢) |
72 | 71 | ad2antll 719 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝑥𝐹𝑚) ∈ 𝑢) |
73 | 67, 72 | eqeltrd 2859 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝐹‘〈𝑛, 𝑚〉) ∈ 𝑢) |
74 | | elpreima 6602 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn (𝑋 × 𝑌) → (〈𝑛, 𝑚〉 ∈ (◡𝐹 “ 𝑢) ↔ (〈𝑛, 𝑚〉 ∈ (𝑋 × 𝑌) ∧ (𝐹‘〈𝑛, 𝑚〉) ∈ 𝑢))) |
75 | 1, 74 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (〈𝑛, 𝑚〉 ∈ (◡𝐹 “ 𝑢) ↔ (〈𝑛, 𝑚〉 ∈ (𝑋 × 𝑌) ∧ (𝐹‘〈𝑛, 𝑚〉) ∈ 𝑢))) |
76 | 75 | ad3antrrr 720 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (〈𝑛, 𝑚〉 ∈ (◡𝐹 “ 𝑢) ↔ (〈𝑛, 𝑚〉 ∈ (𝑋 × 𝑌) ∧ (𝐹‘〈𝑛, 𝑚〉) ∈ 𝑢))) |
77 | 62, 73, 76 | mpbir2and 703 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 〈𝑛, 𝑚〉 ∈ (◡𝐹 “ 𝑢)) |
78 | 77 | ex 403 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ((𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) → 〈𝑛, 𝑚〉 ∈ (◡𝐹 “ 𝑢))) |
79 | 55, 78 | syl5bi 234 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (〈𝑛, 𝑚〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) → 〈𝑛, 𝑚〉 ∈ (◡𝐹 “ 𝑢))) |
80 | 54, 79 | relssdv 5461 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢)) |
81 | | xpeq1 5371 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = {𝑥} → (𝑎 × 𝑏) = ({𝑥} × 𝑏)) |
82 | 81 | eleq2d 2845 |
. . . . . . . . . . . . 13
⊢ (𝑎 = {𝑥} → (〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏) ↔ 〈𝑥, 𝑧〉 ∈ ({𝑥} × 𝑏))) |
83 | 81 | sseq1d 3851 |
. . . . . . . . . . . . 13
⊢ (𝑎 = {𝑥} → ((𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢) ↔ ({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢))) |
84 | 82, 83 | anbi12d 624 |
. . . . . . . . . . . 12
⊢ (𝑎 = {𝑥} → ((〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ (〈𝑥, 𝑧〉 ∈ ({𝑥} × 𝑏) ∧ ({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢)))) |
85 | | xpeq2 5378 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → ({𝑥} × 𝑏) = ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) |
86 | 85 | eleq2d 2845 |
. . . . . . . . . . . . 13
⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (〈𝑥, 𝑧〉 ∈ ({𝑥} × 𝑏) ↔ 〈𝑥, 𝑧〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))) |
87 | 85 | sseq1d 3851 |
. . . . . . . . . . . . 13
⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢) ↔ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢))) |
88 | 86, 87 | anbi12d 624 |
. . . . . . . . . . . 12
⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → ((〈𝑥, 𝑧〉 ∈ ({𝑥} × 𝑏) ∧ ({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ (〈𝑥, 𝑧〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ∧ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢)))) |
89 | 84, 88 | rspc2ev 3526 |
. . . . . . . . . . 11
⊢ (({𝑥} ∈ 𝒫 𝑋 ∧ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ∈ 𝐽 ∧ (〈𝑥, 𝑧〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ∧ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢))) → ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))) |
90 | 35, 42, 52, 80, 89 | syl112anc 1442 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))) |
91 | | opex 5166 |
. . . . . . . . . . 11
⊢
〈𝑥, 𝑧〉 ∈ V |
92 | | eleq1 2847 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 〈𝑥, 𝑧〉 → (𝑣 ∈ (𝑎 × 𝑏) ↔ 〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏))) |
93 | 92 | anbi1d 623 |
. . . . . . . . . . . 12
⊢ (𝑣 = 〈𝑥, 𝑧〉 → ((𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ (〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))) |
94 | 93 | 2rexbidv 3242 |
. . . . . . . . . . 11
⊢ (𝑣 = 〈𝑥, 𝑧〉 → (∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))) |
95 | 91, 94 | elab 3558 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑧〉 ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))} ↔ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))) |
96 | 90, 95 | sylibr 226 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 〈𝑥, 𝑧〉 ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))}) |
97 | 96 | ex 403 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢) → 〈𝑥, 𝑧〉 ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))})) |
98 | 32, 97 | syl5bi 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → ((〈𝑥, 𝑧〉 ∈ (𝑋 × 𝑌) ∧ (𝐹‘〈𝑥, 𝑧〉) ∈ 𝑢) → 〈𝑥, 𝑧〉 ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))})) |
99 | 27, 98 | sylbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑧〉 ∈ (◡𝐹 “ 𝑢) → 〈𝑥, 𝑧〉 ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))})) |
100 | 25, 99 | relssdv 5461 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (◡𝐹 “ 𝑢) ⊆ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))}) |
101 | | ssabral 3894 |
. . . . 5
⊢ ((◡𝐹 “ 𝑢) ⊆ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))} ↔ ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))) |
102 | 100, 101 | sylib 210 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))) |
103 | | txdis1cn.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
104 | | distopon 21213 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ (TopOn‘𝑋)) |
105 | 103, 104 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝒫 𝑋 ∈ (TopOn‘𝑋)) |
106 | 105 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → 𝒫 𝑋 ∈ (TopOn‘𝑋)) |
107 | 2 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → 𝐽 ∈ (TopOn‘𝑌)) |
108 | | eltx 21784 |
. . . . 5
⊢
((𝒫 𝑋 ∈
(TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑌)) → ((◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽) ↔ ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))) |
109 | 106, 107,
108 | syl2anc 579 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → ((◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽) ↔ ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))) |
110 | 102, 109 | mpbird 249 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽)) |
111 | 110 | ralrimiva 3148 |
. 2
⊢ (𝜑 → ∀𝑢 ∈ 𝐾 (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽)) |
112 | | txtopon 21807 |
. . . 4
⊢
((𝒫 𝑋 ∈
(TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑌)) → (𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌))) |
113 | 105, 2, 112 | syl2anc 579 |
. . 3
⊢ (𝜑 → (𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌))) |
114 | | iscn 21451 |
. . 3
⊢
(((𝒫 𝑋
×t 𝐽)
∈ (TopOn‘(𝑋
× 𝑌)) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾))
→ (𝐹 ∈
((𝒫 𝑋
×t 𝐽) Cn
𝐾) ↔ (𝐹:(𝑋 × 𝑌)⟶∪ 𝐾 ∧ ∀𝑢 ∈ 𝐾 (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽)))) |
115 | 113, 7, 114 | syl2anc 579 |
. 2
⊢ (𝜑 → (𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 × 𝑌)⟶∪ 𝐾 ∧ ∀𝑢 ∈ 𝐾 (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽)))) |
116 | 17, 111, 115 | mpbir2and 703 |
1
⊢ (𝜑 → 𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾)) |