Step | Hyp | Ref
| Expression |
1 | | txdis1cn.f |
. . 3
⊢ (𝜑 → 𝐹 Fn (𝑋 × 𝑌)) |
2 | | txdis1cn.j |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑌)) |
3 | 2 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑌)) |
4 | | txdis1cn.k |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ Top) |
5 | | toptopon2 21526 |
. . . . . . . 8
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
6 | 4, 5 | sylib 220 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
7 | 6 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
8 | | txdis1cn.1 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) |
9 | | cnf2 21857 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)
∧ (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)):𝑌⟶∪ 𝐾) |
10 | 3, 7, 8, 9 | syl3anc 1367 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)):𝑌⟶∪ 𝐾) |
11 | | eqid 2821 |
. . . . . 6
⊢ (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) = (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) |
12 | 11 | fmpt 6874 |
. . . . 5
⊢
(∀𝑦 ∈
𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾 ↔ (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)):𝑌⟶∪ 𝐾) |
13 | 10, 12 | sylibr 236 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾) |
14 | 13 | ralrimiva 3182 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾) |
15 | | ffnov 7278 |
. . 3
⊢ (𝐹:(𝑋 × 𝑌)⟶∪ 𝐾 ↔ (𝐹 Fn (𝑋 × 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾)) |
16 | 1, 14, 15 | sylanbrc 585 |
. 2
⊢ (𝜑 → 𝐹:(𝑋 × 𝑌)⟶∪ 𝐾) |
17 | | cnvimass 5949 |
. . . . . . . 8
⊢ (◡𝐹 “ 𝑢) ⊆ dom 𝐹 |
18 | 1 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → 𝐹 Fn (𝑋 × 𝑌)) |
19 | | fndm 6455 |
. . . . . . . . 9
⊢ (𝐹 Fn (𝑋 × 𝑌) → dom 𝐹 = (𝑋 × 𝑌)) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → dom 𝐹 = (𝑋 × 𝑌)) |
21 | 17, 20 | sseqtrid 4019 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (◡𝐹 “ 𝑢) ⊆ (𝑋 × 𝑌)) |
22 | | relxp 5573 |
. . . . . . 7
⊢ Rel
(𝑋 × 𝑌) |
23 | | relss 5656 |
. . . . . . 7
⊢ ((◡𝐹 “ 𝑢) ⊆ (𝑋 × 𝑌) → (Rel (𝑋 × 𝑌) → Rel (◡𝐹 “ 𝑢))) |
24 | 21, 22, 23 | mpisyl 21 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → Rel (◡𝐹 “ 𝑢)) |
25 | | elpreima 6828 |
. . . . . . . 8
⊢ (𝐹 Fn (𝑋 × 𝑌) → (〈𝑥, 𝑧〉 ∈ (◡𝐹 “ 𝑢) ↔ (〈𝑥, 𝑧〉 ∈ (𝑋 × 𝑌) ∧ (𝐹‘〈𝑥, 𝑧〉) ∈ 𝑢))) |
26 | 18, 25 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑧〉 ∈ (◡𝐹 “ 𝑢) ↔ (〈𝑥, 𝑧〉 ∈ (𝑋 × 𝑌) ∧ (𝐹‘〈𝑥, 𝑧〉) ∈ 𝑢))) |
27 | | opelxp 5591 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑧〉 ∈ (𝑋 × 𝑌) ↔ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌)) |
28 | | df-ov 7159 |
. . . . . . . . . . 11
⊢ (𝑥𝐹𝑧) = (𝐹‘〈𝑥, 𝑧〉) |
29 | 28 | eqcomi 2830 |
. . . . . . . . . 10
⊢ (𝐹‘〈𝑥, 𝑧〉) = (𝑥𝐹𝑧) |
30 | 29 | eleq1i 2903 |
. . . . . . . . 9
⊢ ((𝐹‘〈𝑥, 𝑧〉) ∈ 𝑢 ↔ (𝑥𝐹𝑧) ∈ 𝑢) |
31 | 27, 30 | anbi12i 628 |
. . . . . . . 8
⊢
((〈𝑥, 𝑧〉 ∈ (𝑋 × 𝑌) ∧ (𝐹‘〈𝑥, 𝑧〉) ∈ 𝑢) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) |
32 | | simprll 777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑥 ∈ 𝑋) |
33 | | snelpwi 5337 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋 → {𝑥} ∈ 𝒫 𝑋) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑥} ∈ 𝒫 𝑋) |
35 | 11 | mptpreima 6092 |
. . . . . . . . . . . 12
⊢ (◡(𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} |
36 | 8 | adantrr 715 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) |
37 | 36 | ad2ant2r 745 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) |
38 | | simplr 767 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑢 ∈ 𝐾) |
39 | | cnima 21873 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾) ∧ 𝑢 ∈ 𝐾) → (◡(𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) ∈ 𝐽) |
40 | 37, 38, 39 | syl2anc 586 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (◡(𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) ∈ 𝐽) |
41 | 35, 40 | eqeltrrid 2918 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ∈ 𝐽) |
42 | | simprlr 778 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑧 ∈ 𝑌) |
43 | | simprr 771 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (𝑥𝐹𝑧) ∈ 𝑢) |
44 | | vsnid 4602 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ {𝑥} |
45 | | opelxp 5591 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑧〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑥 ∈ {𝑥} ∧ 𝑧 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) |
46 | 44, 45 | mpbiran 707 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑧〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ 𝑧 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) |
47 | | oveq2 7164 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → (𝑥𝐹𝑦) = (𝑥𝐹𝑧)) |
48 | 47 | eleq1d 2897 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → ((𝑥𝐹𝑦) ∈ 𝑢 ↔ (𝑥𝐹𝑧) ∈ 𝑢)) |
49 | 48 | elrab 3680 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ↔ (𝑧 ∈ 𝑌 ∧ (𝑥𝐹𝑧) ∈ 𝑢)) |
50 | 46, 49 | bitri 277 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑧〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑧 ∈ 𝑌 ∧ (𝑥𝐹𝑧) ∈ 𝑢)) |
51 | 42, 43, 50 | sylanbrc 585 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 〈𝑥, 𝑧〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) |
52 | | relxp 5573 |
. . . . . . . . . . . . 13
⊢ Rel
({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) |
53 | 52 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → Rel ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) |
54 | | opelxp 5591 |
. . . . . . . . . . . . 13
⊢
(〈𝑛, 𝑚〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) |
55 | 32 | snssd 4742 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑥} ⊆ 𝑋) |
56 | 55 | sselda 3967 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ 𝑛 ∈ {𝑥}) → 𝑛 ∈ 𝑋) |
57 | 56 | adantrr 715 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑛 ∈ 𝑋) |
58 | | elrabi 3675 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → 𝑚 ∈ 𝑌) |
59 | 58 | ad2antll 727 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑚 ∈ 𝑌) |
60 | 57, 59 | opelxpd 5593 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 〈𝑛, 𝑚〉 ∈ (𝑋 × 𝑌)) |
61 | | df-ov 7159 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛𝐹𝑚) = (𝐹‘〈𝑛, 𝑚〉) |
62 | | elsni 4584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ {𝑥} → 𝑛 = 𝑥) |
63 | 62 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑛 = 𝑥) |
64 | 63 | oveq1d 7171 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝑛𝐹𝑚) = (𝑥𝐹𝑚)) |
65 | 61, 64 | syl5eqr 2870 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝐹‘〈𝑛, 𝑚〉) = (𝑥𝐹𝑚)) |
66 | | oveq2 7164 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑚 → (𝑥𝐹𝑦) = (𝑥𝐹𝑚)) |
67 | 66 | eleq1d 2897 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑚 → ((𝑥𝐹𝑦) ∈ 𝑢 ↔ (𝑥𝐹𝑚) ∈ 𝑢)) |
68 | 67 | elrab 3680 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ↔ (𝑚 ∈ 𝑌 ∧ (𝑥𝐹𝑚) ∈ 𝑢)) |
69 | 68 | simprbi 499 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (𝑥𝐹𝑚) ∈ 𝑢) |
70 | 69 | ad2antll 727 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝑥𝐹𝑚) ∈ 𝑢) |
71 | 65, 70 | eqeltrd 2913 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝐹‘〈𝑛, 𝑚〉) ∈ 𝑢) |
72 | | elpreima 6828 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn (𝑋 × 𝑌) → (〈𝑛, 𝑚〉 ∈ (◡𝐹 “ 𝑢) ↔ (〈𝑛, 𝑚〉 ∈ (𝑋 × 𝑌) ∧ (𝐹‘〈𝑛, 𝑚〉) ∈ 𝑢))) |
73 | 1, 72 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (〈𝑛, 𝑚〉 ∈ (◡𝐹 “ 𝑢) ↔ (〈𝑛, 𝑚〉 ∈ (𝑋 × 𝑌) ∧ (𝐹‘〈𝑛, 𝑚〉) ∈ 𝑢))) |
74 | 73 | ad3antrrr 728 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (〈𝑛, 𝑚〉 ∈ (◡𝐹 “ 𝑢) ↔ (〈𝑛, 𝑚〉 ∈ (𝑋 × 𝑌) ∧ (𝐹‘〈𝑛, 𝑚〉) ∈ 𝑢))) |
75 | 60, 71, 74 | mpbir2and 711 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 〈𝑛, 𝑚〉 ∈ (◡𝐹 “ 𝑢)) |
76 | 75 | ex 415 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ((𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) → 〈𝑛, 𝑚〉 ∈ (◡𝐹 “ 𝑢))) |
77 | 54, 76 | syl5bi 244 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (〈𝑛, 𝑚〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) → 〈𝑛, 𝑚〉 ∈ (◡𝐹 “ 𝑢))) |
78 | 53, 77 | relssdv 5661 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢)) |
79 | | xpeq1 5569 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = {𝑥} → (𝑎 × 𝑏) = ({𝑥} × 𝑏)) |
80 | 79 | eleq2d 2898 |
. . . . . . . . . . . . 13
⊢ (𝑎 = {𝑥} → (〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏) ↔ 〈𝑥, 𝑧〉 ∈ ({𝑥} × 𝑏))) |
81 | 79 | sseq1d 3998 |
. . . . . . . . . . . . 13
⊢ (𝑎 = {𝑥} → ((𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢) ↔ ({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢))) |
82 | 80, 81 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑎 = {𝑥} → ((〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ (〈𝑥, 𝑧〉 ∈ ({𝑥} × 𝑏) ∧ ({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢)))) |
83 | | xpeq2 5576 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → ({𝑥} × 𝑏) = ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) |
84 | 83 | eleq2d 2898 |
. . . . . . . . . . . . 13
⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (〈𝑥, 𝑧〉 ∈ ({𝑥} × 𝑏) ↔ 〈𝑥, 𝑧〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))) |
85 | 83 | sseq1d 3998 |
. . . . . . . . . . . . 13
⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢) ↔ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢))) |
86 | 84, 85 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → ((〈𝑥, 𝑧〉 ∈ ({𝑥} × 𝑏) ∧ ({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ (〈𝑥, 𝑧〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ∧ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢)))) |
87 | 82, 86 | rspc2ev 3635 |
. . . . . . . . . . 11
⊢ (({𝑥} ∈ 𝒫 𝑋 ∧ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ∈ 𝐽 ∧ (〈𝑥, 𝑧〉 ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ∧ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢))) → ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))) |
88 | 34, 41, 51, 78, 87 | syl112anc 1370 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))) |
89 | | opex 5356 |
. . . . . . . . . . 11
⊢
〈𝑥, 𝑧〉 ∈ V |
90 | | eleq1 2900 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 〈𝑥, 𝑧〉 → (𝑣 ∈ (𝑎 × 𝑏) ↔ 〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏))) |
91 | 90 | anbi1d 631 |
. . . . . . . . . . . 12
⊢ (𝑣 = 〈𝑥, 𝑧〉 → ((𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ (〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))) |
92 | 91 | 2rexbidv 3300 |
. . . . . . . . . . 11
⊢ (𝑣 = 〈𝑥, 𝑧〉 → (∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))) |
93 | 89, 92 | elab 3667 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑧〉 ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))} ↔ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (〈𝑥, 𝑧〉 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))) |
94 | 88, 93 | sylibr 236 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 〈𝑥, 𝑧〉 ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))}) |
95 | 94 | ex 415 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢) → 〈𝑥, 𝑧〉 ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))})) |
96 | 31, 95 | syl5bi 244 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → ((〈𝑥, 𝑧〉 ∈ (𝑋 × 𝑌) ∧ (𝐹‘〈𝑥, 𝑧〉) ∈ 𝑢) → 〈𝑥, 𝑧〉 ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))})) |
97 | 26, 96 | sylbid 242 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (〈𝑥, 𝑧〉 ∈ (◡𝐹 “ 𝑢) → 〈𝑥, 𝑧〉 ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))})) |
98 | 24, 97 | relssdv 5661 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (◡𝐹 “ 𝑢) ⊆ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))}) |
99 | | ssabral 4042 |
. . . . 5
⊢ ((◡𝐹 “ 𝑢) ⊆ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))} ↔ ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))) |
100 | 98, 99 | sylib 220 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))) |
101 | | txdis1cn.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
102 | | distopon 21605 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ (TopOn‘𝑋)) |
103 | 101, 102 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝒫 𝑋 ∈ (TopOn‘𝑋)) |
104 | 103 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → 𝒫 𝑋 ∈ (TopOn‘𝑋)) |
105 | 2 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → 𝐽 ∈ (TopOn‘𝑌)) |
106 | | eltx 22176 |
. . . . 5
⊢
((𝒫 𝑋 ∈
(TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑌)) → ((◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽) ↔ ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))) |
107 | 104, 105,
106 | syl2anc 586 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → ((◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽) ↔ ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))) |
108 | 100, 107 | mpbird 259 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽)) |
109 | 108 | ralrimiva 3182 |
. 2
⊢ (𝜑 → ∀𝑢 ∈ 𝐾 (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽)) |
110 | | txtopon 22199 |
. . . 4
⊢
((𝒫 𝑋 ∈
(TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑌)) → (𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌))) |
111 | 103, 2, 110 | syl2anc 586 |
. . 3
⊢ (𝜑 → (𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌))) |
112 | | iscn 21843 |
. . 3
⊢
(((𝒫 𝑋
×t 𝐽)
∈ (TopOn‘(𝑋
× 𝑌)) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾))
→ (𝐹 ∈
((𝒫 𝑋
×t 𝐽) Cn
𝐾) ↔ (𝐹:(𝑋 × 𝑌)⟶∪ 𝐾 ∧ ∀𝑢 ∈ 𝐾 (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽)))) |
113 | 111, 6, 112 | syl2anc 586 |
. 2
⊢ (𝜑 → (𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 × 𝑌)⟶∪ 𝐾 ∧ ∀𝑢 ∈ 𝐾 (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽)))) |
114 | 16, 109, 113 | mpbir2and 711 |
1
⊢ (𝜑 → 𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾)) |