Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  txdis1cn GIF version

Theorem txdis1cn 12506
 Description: A function is jointly continuous on a discrete left topology iff it is continuous as a function of its right argument, for each fixed left value. (Contributed by Mario Carneiro, 19-Sep-2015.)
Hypotheses
Ref Expression
txdis1cn.x (𝜑𝑋𝑉)
txdis1cn.j (𝜑𝐽 ∈ (TopOn‘𝑌))
txdis1cn.k (𝜑𝐾 ∈ Top)
txdis1cn.f (𝜑𝐹 Fn (𝑋 × 𝑌))
txdis1cn.1 ((𝜑𝑥𝑋) → (𝑦𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
Assertion
Ref Expression
txdis1cn (𝜑𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾))
Distinct variable groups:   𝑥,𝑦,𝐹   𝑥,𝐽   𝑥,𝑋,𝑦   𝑥,𝐾,𝑦   𝜑,𝑥   𝑥,𝑌,𝑦
Allowed substitution hints:   𝜑(𝑦)   𝐽(𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem txdis1cn
Dummy variables 𝑎 𝑏 𝑚 𝑛 𝑢 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 txdis1cn.f . . 3 (𝜑𝐹 Fn (𝑋 × 𝑌))
2 txdis1cn.j . . . . . . 7 (𝜑𝐽 ∈ (TopOn‘𝑌))
32adantr 274 . . . . . 6 ((𝜑𝑥𝑋) → 𝐽 ∈ (TopOn‘𝑌))
4 txdis1cn.k . . . . . . . 8 (𝜑𝐾 ∈ Top)
5 toptopon2 12245 . . . . . . . 8 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘ 𝐾))
64, 5sylib 121 . . . . . . 7 (𝜑𝐾 ∈ (TopOn‘ 𝐾))
76adantr 274 . . . . . 6 ((𝜑𝑥𝑋) → 𝐾 ∈ (TopOn‘ 𝐾))
8 txdis1cn.1 . . . . . 6 ((𝜑𝑥𝑋) → (𝑦𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
9 cnf2 12433 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘ 𝐾) ∧ (𝑦𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) → (𝑦𝑌 ↦ (𝑥𝐹𝑦)):𝑌 𝐾)
103, 7, 8, 9syl3anc 1217 . . . . 5 ((𝜑𝑥𝑋) → (𝑦𝑌 ↦ (𝑥𝐹𝑦)):𝑌 𝐾)
11 eqid 2140 . . . . . 6 (𝑦𝑌 ↦ (𝑥𝐹𝑦)) = (𝑦𝑌 ↦ (𝑥𝐹𝑦))
1211fmpt 5579 . . . . 5 (∀𝑦𝑌 (𝑥𝐹𝑦) ∈ 𝐾 ↔ (𝑦𝑌 ↦ (𝑥𝐹𝑦)):𝑌 𝐾)
1310, 12sylibr 133 . . . 4 ((𝜑𝑥𝑋) → ∀𝑦𝑌 (𝑥𝐹𝑦) ∈ 𝐾)
1413ralrimiva 2509 . . 3 (𝜑 → ∀𝑥𝑋𝑦𝑌 (𝑥𝐹𝑦) ∈ 𝐾)
15 ffnov 5884 . . 3 (𝐹:(𝑋 × 𝑌)⟶ 𝐾 ↔ (𝐹 Fn (𝑋 × 𝑌) ∧ ∀𝑥𝑋𝑦𝑌 (𝑥𝐹𝑦) ∈ 𝐾))
161, 14, 15sylanbrc 414 . 2 (𝜑𝐹:(𝑋 × 𝑌)⟶ 𝐾)
17 cnvimass 4911 . . . . . . . 8 (𝐹𝑢) ⊆ dom 𝐹
181adantr 274 . . . . . . . . 9 ((𝜑𝑢𝐾) → 𝐹 Fn (𝑋 × 𝑌))
19 fndm 5231 . . . . . . . . 9 (𝐹 Fn (𝑋 × 𝑌) → dom 𝐹 = (𝑋 × 𝑌))
2018, 19syl 14 . . . . . . . 8 ((𝜑𝑢𝐾) → dom 𝐹 = (𝑋 × 𝑌))
2117, 20sseqtrid 3153 . . . . . . 7 ((𝜑𝑢𝐾) → (𝐹𝑢) ⊆ (𝑋 × 𝑌))
22 relxp 4657 . . . . . . 7 Rel (𝑋 × 𝑌)
23 relss 4635 . . . . . . 7 ((𝐹𝑢) ⊆ (𝑋 × 𝑌) → (Rel (𝑋 × 𝑌) → Rel (𝐹𝑢)))
2421, 22, 23mpisyl 1423 . . . . . 6 ((𝜑𝑢𝐾) → Rel (𝐹𝑢))
25 elpreima 5548 . . . . . . . 8 (𝐹 Fn (𝑋 × 𝑌) → (⟨𝑥, 𝑧⟩ ∈ (𝐹𝑢) ↔ (⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢)))
2618, 25syl 14 . . . . . . 7 ((𝜑𝑢𝐾) → (⟨𝑥, 𝑧⟩ ∈ (𝐹𝑢) ↔ (⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢)))
27 opelxp 4578 . . . . . . . . 9 (⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ↔ (𝑥𝑋𝑧𝑌))
28 df-ov 5786 . . . . . . . . . . 11 (𝑥𝐹𝑧) = (𝐹‘⟨𝑥, 𝑧⟩)
2928eqcomi 2144 . . . . . . . . . 10 (𝐹‘⟨𝑥, 𝑧⟩) = (𝑥𝐹𝑧)
3029eleq1i 2206 . . . . . . . . 9 ((𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢 ↔ (𝑥𝐹𝑧) ∈ 𝑢)
3127, 30anbi12i 456 . . . . . . . 8 ((⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢) ↔ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢))
32 simprll 527 . . . . . . . . . . . 12 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑥𝑋)
33 snelpwi 4143 . . . . . . . . . . . 12 (𝑥𝑋 → {𝑥} ∈ 𝒫 𝑋)
3432, 33syl 14 . . . . . . . . . . 11 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑥} ∈ 𝒫 𝑋)
3511mptpreima 5041 . . . . . . . . . . . 12 ((𝑦𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) = {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}
368adantrr 471 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝑋𝑧𝑌)) → (𝑦𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
3736ad2ant2r 501 . . . . . . . . . . . . 13 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (𝑦𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
38 simplr 520 . . . . . . . . . . . . 13 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑢𝐾)
39 cnima 12448 . . . . . . . . . . . . 13 (((𝑦𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾) ∧ 𝑢𝐾) → ((𝑦𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) ∈ 𝐽)
4037, 38, 39syl2anc 409 . . . . . . . . . . . 12 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ((𝑦𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) ∈ 𝐽)
4135, 40eqeltrrid 2228 . . . . . . . . . . 11 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ∈ 𝐽)
42 simprlr 528 . . . . . . . . . . . 12 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑧𝑌)
43 simprr 522 . . . . . . . . . . . 12 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (𝑥𝐹𝑧) ∈ 𝑢)
44 vsnid 3565 . . . . . . . . . . . . . 14 𝑥 ∈ {𝑥}
45 opelxp 4578 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑥 ∈ {𝑥} ∧ 𝑧 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
4644, 45mpbiran 925 . . . . . . . . . . . . 13 (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ 𝑧 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})
47 oveq2 5791 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 → (𝑥𝐹𝑦) = (𝑥𝐹𝑧))
4847eleq1d 2209 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → ((𝑥𝐹𝑦) ∈ 𝑢 ↔ (𝑥𝐹𝑧) ∈ 𝑢))
4948elrab 2845 . . . . . . . . . . . . 13 (𝑧 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ↔ (𝑧𝑌 ∧ (𝑥𝐹𝑧) ∈ 𝑢))
5046, 49bitri 183 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑧𝑌 ∧ (𝑥𝐹𝑧) ∈ 𝑢))
5142, 43, 50sylanbrc 414 . . . . . . . . . . 11 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
52 relxp 4657 . . . . . . . . . . . . 13 Rel ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})
5352a1i 9 . . . . . . . . . . . 12 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → Rel ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
54 opelxp 4578 . . . . . . . . . . . . 13 (⟨𝑛, 𝑚⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
5532snssd 3674 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑥} ⊆ 𝑋)
5655sselda 3103 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ 𝑛 ∈ {𝑥}) → 𝑛𝑋)
5756adantrr 471 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑛𝑋)
58 elrabi 2842 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → 𝑚𝑌)
5958ad2antll 483 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑚𝑌)
6057, 59opelxpd 4581 . . . . . . . . . . . . . . 15 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → ⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌))
61 df-ov 5786 . . . . . . . . . . . . . . . . 17 (𝑛𝐹𝑚) = (𝐹‘⟨𝑛, 𝑚⟩)
62 elsni 3551 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ {𝑥} → 𝑛 = 𝑥)
6362ad2antrl 482 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑛 = 𝑥)
6463oveq1d 5798 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝑛𝐹𝑚) = (𝑥𝐹𝑚))
6561, 64syl5eqr 2187 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝐹‘⟨𝑛, 𝑚⟩) = (𝑥𝐹𝑚))
66 oveq2 5791 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑚 → (𝑥𝐹𝑦) = (𝑥𝐹𝑚))
6766eleq1d 2209 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑚 → ((𝑥𝐹𝑦) ∈ 𝑢 ↔ (𝑥𝐹𝑚) ∈ 𝑢))
6867elrab 2845 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ↔ (𝑚𝑌 ∧ (𝑥𝐹𝑚) ∈ 𝑢))
6968simprbi 273 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (𝑥𝐹𝑚) ∈ 𝑢)
7069ad2antll 483 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝑥𝐹𝑚) ∈ 𝑢)
7165, 70eqeltrd 2217 . . . . . . . . . . . . . . 15 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)
72 elpreima 5548 . . . . . . . . . . . . . . . . 17 (𝐹 Fn (𝑋 × 𝑌) → (⟨𝑛, 𝑚⟩ ∈ (𝐹𝑢) ↔ (⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)))
731, 72syl 14 . . . . . . . . . . . . . . . 16 (𝜑 → (⟨𝑛, 𝑚⟩ ∈ (𝐹𝑢) ↔ (⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)))
7473ad3antrrr 484 . . . . . . . . . . . . . . 15 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (⟨𝑛, 𝑚⟩ ∈ (𝐹𝑢) ↔ (⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)))
7560, 71, 74mpbir2and 929 . . . . . . . . . . . . . 14 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → ⟨𝑛, 𝑚⟩ ∈ (𝐹𝑢))
7675ex 114 . . . . . . . . . . . . 13 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ((𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) → ⟨𝑛, 𝑚⟩ ∈ (𝐹𝑢)))
7754, 76syl5bi 151 . . . . . . . . . . . 12 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (⟨𝑛, 𝑚⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) → ⟨𝑛, 𝑚⟩ ∈ (𝐹𝑢)))
7853, 77relssdv 4640 . . . . . . . . . . 11 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (𝐹𝑢))
79 xpeq1 4562 . . . . . . . . . . . . . 14 (𝑎 = {𝑥} → (𝑎 × 𝑏) = ({𝑥} × 𝑏))
8079eleq2d 2210 . . . . . . . . . . . . 13 (𝑎 = {𝑥} → (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ↔ ⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏)))
8179sseq1d 3132 . . . . . . . . . . . . 13 (𝑎 = {𝑥} → ((𝑎 × 𝑏) ⊆ (𝐹𝑢) ↔ ({𝑥} × 𝑏) ⊆ (𝐹𝑢)))
8280, 81anbi12d 465 . . . . . . . . . . . 12 (𝑎 = {𝑥} → ((⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)) ↔ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏) ∧ ({𝑥} × 𝑏) ⊆ (𝐹𝑢))))
83 xpeq2 4563 . . . . . . . . . . . . . 14 (𝑏 = {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → ({𝑥} × 𝑏) = ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
8483eleq2d 2210 . . . . . . . . . . . . 13 (𝑏 = {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏) ↔ ⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})))
8583sseq1d 3132 . . . . . . . . . . . . 13 (𝑏 = {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (({𝑥} × 𝑏) ⊆ (𝐹𝑢) ↔ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (𝐹𝑢)))
8684, 85anbi12d 465 . . . . . . . . . . . 12 (𝑏 = {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → ((⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏) ∧ ({𝑥} × 𝑏) ⊆ (𝐹𝑢)) ↔ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ∧ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (𝐹𝑢))))
8782, 86rspc2ev 2809 . . . . . . . . . . 11 (({𝑥} ∈ 𝒫 𝑋 ∧ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ∈ 𝐽 ∧ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ∧ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (𝐹𝑢))) → ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)))
8834, 41, 51, 78, 87syl112anc 1221 . . . . . . . . . 10 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)))
89 vex 2693 . . . . . . . . . . . 12 𝑥 ∈ V
90 vex 2693 . . . . . . . . . . . 12 𝑧 ∈ V
9189, 90opex 4160 . . . . . . . . . . 11 𝑥, 𝑧⟩ ∈ V
92 eleq1 2203 . . . . . . . . . . . . 13 (𝑣 = ⟨𝑥, 𝑧⟩ → (𝑣 ∈ (𝑎 × 𝑏) ↔ ⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏)))
9392anbi1d 461 . . . . . . . . . . . 12 (𝑣 = ⟨𝑥, 𝑧⟩ → ((𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)) ↔ (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))))
94932rexbidv 2464 . . . . . . . . . . 11 (𝑣 = ⟨𝑥, 𝑧⟩ → (∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)) ↔ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))))
9591, 94elab 2833 . . . . . . . . . 10 (⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))} ↔ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)))
9688, 95sylibr 133 . . . . . . . . 9 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))})
9796ex 114 . . . . . . . 8 ((𝜑𝑢𝐾) → (((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))}))
9831, 97syl5bi 151 . . . . . . 7 ((𝜑𝑢𝐾) → ((⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))}))
9926, 98sylbid 149 . . . . . 6 ((𝜑𝑢𝐾) → (⟨𝑥, 𝑧⟩ ∈ (𝐹𝑢) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))}))
10024, 99relssdv 4640 . . . . 5 ((𝜑𝑢𝐾) → (𝐹𝑢) ⊆ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))})
101 ssabral 3174 . . . . 5 ((𝐹𝑢) ⊆ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))} ↔ ∀𝑣 ∈ (𝐹𝑢)∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)))
102100, 101sylib 121 . . . 4 ((𝜑𝑢𝐾) → ∀𝑣 ∈ (𝐹𝑢)∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)))
103 txdis1cn.x . . . . . . 7 (𝜑𝑋𝑉)
104 distopon 12315 . . . . . . 7 (𝑋𝑉 → 𝒫 𝑋 ∈ (TopOn‘𝑋))
105103, 104syl 14 . . . . . 6 (𝜑 → 𝒫 𝑋 ∈ (TopOn‘𝑋))
106105adantr 274 . . . . 5 ((𝜑𝑢𝐾) → 𝒫 𝑋 ∈ (TopOn‘𝑋))
1072adantr 274 . . . . 5 ((𝜑𝑢𝐾) → 𝐽 ∈ (TopOn‘𝑌))
108 eltx 12487 . . . . 5 ((𝒫 𝑋 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑌)) → ((𝐹𝑢) ∈ (𝒫 𝑋 ×t 𝐽) ↔ ∀𝑣 ∈ (𝐹𝑢)∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))))
109106, 107, 108syl2anc 409 . . . 4 ((𝜑𝑢𝐾) → ((𝐹𝑢) ∈ (𝒫 𝑋 ×t 𝐽) ↔ ∀𝑣 ∈ (𝐹𝑢)∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))))
110102, 109mpbird 166 . . 3 ((𝜑𝑢𝐾) → (𝐹𝑢) ∈ (𝒫 𝑋 ×t 𝐽))
111110ralrimiva 2509 . 2 (𝜑 → ∀𝑢𝐾 (𝐹𝑢) ∈ (𝒫 𝑋 ×t 𝐽))
112 txtopon 12490 . . . 4 ((𝒫 𝑋 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑌)) → (𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌)))
113105, 2, 112syl2anc 409 . . 3 (𝜑 → (𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌)))
114 iscn 12425 . . 3 (((𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐾 ∈ (TopOn‘ 𝐾)) → (𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 × 𝑌)⟶ 𝐾 ∧ ∀𝑢𝐾 (𝐹𝑢) ∈ (𝒫 𝑋 ×t 𝐽))))
115113, 6, 114syl2anc 409 . 2 (𝜑 → (𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 × 𝑌)⟶ 𝐾 ∧ ∀𝑢𝐾 (𝐹𝑢) ∈ (𝒫 𝑋 ×t 𝐽))))
11616, 111, 115mpbir2and 929 1 (𝜑𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332   ∈ wcel 1481  {cab 2126  ∀wral 2417  ∃wrex 2418  {crab 2421   ⊆ wss 3077  𝒫 cpw 3516  {csn 3533  ⟨cop 3536  ∪ cuni 3745   ↦ cmpt 3998   × cxp 4546  ◡ccnv 4547  dom cdm 4548   “ cima 4551  Rel wrel 4553   Fn wfn 5127  ⟶wf 5128  ‘cfv 5132  (class class class)co 5783  Topctop 12223  TopOnctopon 12236   Cn ccn 12413   ×t ctx 12480 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4052  ax-sep 4055  ax-pow 4107  ax-pr 4140  ax-un 4364  ax-setind 4461 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-iun 3824  df-br 3939  df-opab 3999  df-mpt 4000  df-id 4224  df-xp 4554  df-rel 4555  df-cnv 4556  df-co 4557  df-dm 4558  df-rn 4559  df-res 4560  df-ima 4561  df-iota 5097  df-fun 5134  df-fn 5135  df-f 5136  df-f1 5137  df-fo 5138  df-f1o 5139  df-fv 5140  df-ov 5786  df-oprab 5787  df-mpo 5788  df-1st 6047  df-2nd 6048  df-map 6553  df-topgen 12200  df-top 12224  df-topon 12237  df-bases 12269  df-cn 12416  df-tx 12481 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator