MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  txdis1cn Structured version   Visualization version   GIF version

Theorem txdis1cn 21486
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 480 . . . . . 6 ((𝜑𝑥𝑋) → 𝐽 ∈ (TopOn‘𝑌))
4 txdis1cn.k . . . . . . . 8 (𝜑𝐾 ∈ Top)
5 eqid 2651 . . . . . . . . 9 𝐾 = 𝐾
65toptopon 20770 . . . . . . . 8 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘ 𝐾))
74, 6sylib 208 . . . . . . 7 (𝜑𝐾 ∈ (TopOn‘ 𝐾))
87adantr 480 . . . . . 6 ((𝜑𝑥𝑋) → 𝐾 ∈ (TopOn‘ 𝐾))
9 txdis1cn.1 . . . . . 6 ((𝜑𝑥𝑋) → (𝑦𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
10 cnf2 21101 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘ 𝐾) ∧ (𝑦𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) → (𝑦𝑌 ↦ (𝑥𝐹𝑦)):𝑌 𝐾)
113, 8, 9, 10syl3anc 1366 . . . . 5 ((𝜑𝑥𝑋) → (𝑦𝑌 ↦ (𝑥𝐹𝑦)):𝑌 𝐾)
12 eqid 2651 . . . . . 6 (𝑦𝑌 ↦ (𝑥𝐹𝑦)) = (𝑦𝑌 ↦ (𝑥𝐹𝑦))
1312fmpt 6421 . . . . 5 (∀𝑦𝑌 (𝑥𝐹𝑦) ∈ 𝐾 ↔ (𝑦𝑌 ↦ (𝑥𝐹𝑦)):𝑌 𝐾)
1411, 13sylibr 224 . . . 4 ((𝜑𝑥𝑋) → ∀𝑦𝑌 (𝑥𝐹𝑦) ∈ 𝐾)
1514ralrimiva 2995 . . 3 (𝜑 → ∀𝑥𝑋𝑦𝑌 (𝑥𝐹𝑦) ∈ 𝐾)
16 ffnov 6806 . . 3 (𝐹:(𝑋 × 𝑌)⟶ 𝐾 ↔ (𝐹 Fn (𝑋 × 𝑌) ∧ ∀𝑥𝑋𝑦𝑌 (𝑥𝐹𝑦) ∈ 𝐾))
171, 15, 16sylanbrc 699 . 2 (𝜑𝐹:(𝑋 × 𝑌)⟶ 𝐾)
18 cnvimass 5520 . . . . . . . 8 (𝐹𝑢) ⊆ dom 𝐹
191adantr 480 . . . . . . . . 9 ((𝜑𝑢𝐾) → 𝐹 Fn (𝑋 × 𝑌))
20 fndm 6028 . . . . . . . . 9 (𝐹 Fn (𝑋 × 𝑌) → dom 𝐹 = (𝑋 × 𝑌))
2119, 20syl 17 . . . . . . . 8 ((𝜑𝑢𝐾) → dom 𝐹 = (𝑋 × 𝑌))
2218, 21syl5sseq 3686 . . . . . . 7 ((𝜑𝑢𝐾) → (𝐹𝑢) ⊆ (𝑋 × 𝑌))
23 relxp 5160 . . . . . . 7 Rel (𝑋 × 𝑌)
24 relss 5240 . . . . . . 7 ((𝐹𝑢) ⊆ (𝑋 × 𝑌) → (Rel (𝑋 × 𝑌) → Rel (𝐹𝑢)))
2522, 23, 24mpisyl 21 . . . . . 6 ((𝜑𝑢𝐾) → Rel (𝐹𝑢))
26 elpreima 6377 . . . . . . . 8 (𝐹 Fn (𝑋 × 𝑌) → (⟨𝑥, 𝑧⟩ ∈ (𝐹𝑢) ↔ (⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢)))
2719, 26syl 17 . . . . . . 7 ((𝜑𝑢𝐾) → (⟨𝑥, 𝑧⟩ ∈ (𝐹𝑢) ↔ (⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢)))
28 opelxp 5180 . . . . . . . . 9 (⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ↔ (𝑥𝑋𝑧𝑌))
29 df-ov 6693 . . . . . . . . . . 11 (𝑥𝐹𝑧) = (𝐹‘⟨𝑥, 𝑧⟩)
3029eqcomi 2660 . . . . . . . . . 10 (𝐹‘⟨𝑥, 𝑧⟩) = (𝑥𝐹𝑧)
3130eleq1i 2721 . . . . . . . . 9 ((𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢 ↔ (𝑥𝐹𝑧) ∈ 𝑢)
3228, 31anbi12i 733 . . . . . . . 8 ((⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢) ↔ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢))
33 simprll 819 . . . . . . . . . . . 12 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑥𝑋)
34 snelpwi 4942 . . . . . . . . . . . 12 (𝑥𝑋 → {𝑥} ∈ 𝒫 𝑋)
3533, 34syl 17 . . . . . . . . . . 11 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑥} ∈ 𝒫 𝑋)
3612mptpreima 5666 . . . . . . . . . . . 12 ((𝑦𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) = {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}
379adantrr 753 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥𝑋𝑧𝑌)) → (𝑦𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
3837ad2ant2r 798 . . . . . . . . . . . . 13 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (𝑦𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
39 simplr 807 . . . . . . . . . . . . 13 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑢𝐾)
40 cnima 21117 . . . . . . . . . . . . 13 (((𝑦𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾) ∧ 𝑢𝐾) → ((𝑦𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) ∈ 𝐽)
4138, 39, 40syl2anc 694 . . . . . . . . . . . 12 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ((𝑦𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) ∈ 𝐽)
4236, 41syl5eqelr 2735 . . . . . . . . . . 11 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ∈ 𝐽)
43 simprlr 820 . . . . . . . . . . . 12 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑧𝑌)
44 simprr 811 . . . . . . . . . . . 12 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (𝑥𝐹𝑧) ∈ 𝑢)
45 vsnid 4242 . . . . . . . . . . . . . 14 𝑥 ∈ {𝑥}
46 opelxp 5180 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑥 ∈ {𝑥} ∧ 𝑧 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
4745, 46mpbiran 973 . . . . . . . . . . . . 13 (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ 𝑧 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})
48 oveq2 6698 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 → (𝑥𝐹𝑦) = (𝑥𝐹𝑧))
4948eleq1d 2715 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → ((𝑥𝐹𝑦) ∈ 𝑢 ↔ (𝑥𝐹𝑧) ∈ 𝑢))
5049elrab 3396 . . . . . . . . . . . . 13 (𝑧 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ↔ (𝑧𝑌 ∧ (𝑥𝐹𝑧) ∈ 𝑢))
5147, 50bitri 264 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑧𝑌 ∧ (𝑥𝐹𝑧) ∈ 𝑢))
5243, 44, 51sylanbrc 699 . . . . . . . . . . 11 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
53 relxp 5160 . . . . . . . . . . . . 13 Rel ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})
5453a1i 11 . . . . . . . . . . . 12 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → Rel ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
55 opelxp 5180 . . . . . . . . . . . . 13 (⟨𝑛, 𝑚⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
5633snssd 4372 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑥} ⊆ 𝑋)
5756sselda 3636 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ 𝑛 ∈ {𝑥}) → 𝑛𝑋)
5857adantrr 753 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑛𝑋)
59 elrabi 3391 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → 𝑚𝑌)
6059ad2antll 765 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑚𝑌)
61 opelxp 5180 . . . . . . . . . . . . . . . 16 (⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌) ↔ (𝑛𝑋𝑚𝑌))
6258, 60, 61sylanbrc 699 . . . . . . . . . . . . . . 15 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → ⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌))
63 df-ov 6693 . . . . . . . . . . . . . . . . 17 (𝑛𝐹𝑚) = (𝐹‘⟨𝑛, 𝑚⟩)
64 elsni 4227 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ {𝑥} → 𝑛 = 𝑥)
6564ad2antrl 764 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑛 = 𝑥)
6665oveq1d 6705 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝑛𝐹𝑚) = (𝑥𝐹𝑚))
6763, 66syl5eqr 2699 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝐹‘⟨𝑛, 𝑚⟩) = (𝑥𝐹𝑚))
68 oveq2 6698 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑚 → (𝑥𝐹𝑦) = (𝑥𝐹𝑚))
6968eleq1d 2715 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑚 → ((𝑥𝐹𝑦) ∈ 𝑢 ↔ (𝑥𝐹𝑚) ∈ 𝑢))
7069elrab 3396 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ↔ (𝑚𝑌 ∧ (𝑥𝐹𝑚) ∈ 𝑢))
7170simprbi 479 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (𝑥𝐹𝑚) ∈ 𝑢)
7271ad2antll 765 . . . . . . . . . . . . . . . 16 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝑥𝐹𝑚) ∈ 𝑢)
7367, 72eqeltrd 2730 . . . . . . . . . . . . . . 15 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)
74 elpreima 6377 . . . . . . . . . . . . . . . . 17 (𝐹 Fn (𝑋 × 𝑌) → (⟨𝑛, 𝑚⟩ ∈ (𝐹𝑢) ↔ (⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)))
751, 74syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (⟨𝑛, 𝑚⟩ ∈ (𝐹𝑢) ↔ (⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)))
7675ad3antrrr 766 . . . . . . . . . . . . . . 15 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (⟨𝑛, 𝑚⟩ ∈ (𝐹𝑢) ↔ (⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)))
7762, 73, 76mpbir2and 977 . . . . . . . . . . . . . 14 ((((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → ⟨𝑛, 𝑚⟩ ∈ (𝐹𝑢))
7877ex 449 . . . . . . . . . . . . 13 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ((𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) → ⟨𝑛, 𝑚⟩ ∈ (𝐹𝑢)))
7955, 78syl5bi 232 . . . . . . . . . . . 12 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (⟨𝑛, 𝑚⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) → ⟨𝑛, 𝑚⟩ ∈ (𝐹𝑢)))
8054, 79relssdv 5246 . . . . . . . . . . 11 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (𝐹𝑢))
81 xpeq1 5157 . . . . . . . . . . . . . 14 (𝑎 = {𝑥} → (𝑎 × 𝑏) = ({𝑥} × 𝑏))
8281eleq2d 2716 . . . . . . . . . . . . 13 (𝑎 = {𝑥} → (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ↔ ⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏)))
8381sseq1d 3665 . . . . . . . . . . . . 13 (𝑎 = {𝑥} → ((𝑎 × 𝑏) ⊆ (𝐹𝑢) ↔ ({𝑥} × 𝑏) ⊆ (𝐹𝑢)))
8482, 83anbi12d 747 . . . . . . . . . . . 12 (𝑎 = {𝑥} → ((⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)) ↔ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏) ∧ ({𝑥} × 𝑏) ⊆ (𝐹𝑢))))
85 xpeq2 5163 . . . . . . . . . . . . . 14 (𝑏 = {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → ({𝑥} × 𝑏) = ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
8685eleq2d 2716 . . . . . . . . . . . . 13 (𝑏 = {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏) ↔ ⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})))
8785sseq1d 3665 . . . . . . . . . . . . 13 (𝑏 = {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (({𝑥} × 𝑏) ⊆ (𝐹𝑢) ↔ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (𝐹𝑢)))
8886, 87anbi12d 747 . . . . . . . . . . . 12 (𝑏 = {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → ((⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏) ∧ ({𝑥} × 𝑏) ⊆ (𝐹𝑢)) ↔ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ∧ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (𝐹𝑢))))
8984, 88rspc2ev 3355 . . . . . . . . . . 11 (({𝑥} ∈ 𝒫 𝑋 ∧ {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ∈ 𝐽 ∧ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ∧ ({𝑥} × {𝑦𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (𝐹𝑢))) → ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)))
9035, 42, 52, 80, 89syl112anc 1370 . . . . . . . . . 10 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)))
91 opex 4962 . . . . . . . . . . 11 𝑥, 𝑧⟩ ∈ V
92 eleq1 2718 . . . . . . . . . . . . 13 (𝑣 = ⟨𝑥, 𝑧⟩ → (𝑣 ∈ (𝑎 × 𝑏) ↔ ⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏)))
9392anbi1d 741 . . . . . . . . . . . 12 (𝑣 = ⟨𝑥, 𝑧⟩ → ((𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)) ↔ (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))))
94932rexbidv 3086 . . . . . . . . . . 11 (𝑣 = ⟨𝑥, 𝑧⟩ → (∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)) ↔ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))))
9591, 94elab 3382 . . . . . . . . . 10 (⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))} ↔ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)))
9690, 95sylibr 224 . . . . . . . . 9 (((𝜑𝑢𝐾) ∧ ((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))})
9796ex 449 . . . . . . . 8 ((𝜑𝑢𝐾) → (((𝑥𝑋𝑧𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))}))
9832, 97syl5bi 232 . . . . . . 7 ((𝜑𝑢𝐾) → ((⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))}))
9927, 98sylbid 230 . . . . . 6 ((𝜑𝑢𝐾) → (⟨𝑥, 𝑧⟩ ∈ (𝐹𝑢) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))}))
10025, 99relssdv 5246 . . . . 5 ((𝜑𝑢𝐾) → (𝐹𝑢) ⊆ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))})
101 ssabral 3706 . . . . 5 ((𝐹𝑢) ⊆ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))} ↔ ∀𝑣 ∈ (𝐹𝑢)∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)))
102100, 101sylib 208 . . . 4 ((𝜑𝑢𝐾) → ∀𝑣 ∈ (𝐹𝑢)∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢)))
103 txdis1cn.x . . . . . . 7 (𝜑𝑋𝑉)
104 distopon 20849 . . . . . . 7 (𝑋𝑉 → 𝒫 𝑋 ∈ (TopOn‘𝑋))
105103, 104syl 17 . . . . . 6 (𝜑 → 𝒫 𝑋 ∈ (TopOn‘𝑋))
106105adantr 480 . . . . 5 ((𝜑𝑢𝐾) → 𝒫 𝑋 ∈ (TopOn‘𝑋))
1072adantr 480 . . . . 5 ((𝜑𝑢𝐾) → 𝐽 ∈ (TopOn‘𝑌))
108 eltx 21419 . . . . 5 ((𝒫 𝑋 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑌)) → ((𝐹𝑢) ∈ (𝒫 𝑋 ×t 𝐽) ↔ ∀𝑣 ∈ (𝐹𝑢)∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))))
109106, 107, 108syl2anc 694 . . . 4 ((𝜑𝑢𝐾) → ((𝐹𝑢) ∈ (𝒫 𝑋 ×t 𝐽) ↔ ∀𝑣 ∈ (𝐹𝑢)∃𝑎 ∈ 𝒫 𝑋𝑏𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐹𝑢))))
110102, 109mpbird 247 . . 3 ((𝜑𝑢𝐾) → (𝐹𝑢) ∈ (𝒫 𝑋 ×t 𝐽))
111110ralrimiva 2995 . 2 (𝜑 → ∀𝑢𝐾 (𝐹𝑢) ∈ (𝒫 𝑋 ×t 𝐽))
112 txtopon 21442 . . . 4 ((𝒫 𝑋 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑌)) → (𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌)))
113105, 2, 112syl2anc 694 . . 3 (𝜑 → (𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌)))
114 iscn 21087 . . 3 (((𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐾 ∈ (TopOn‘ 𝐾)) → (𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 × 𝑌)⟶ 𝐾 ∧ ∀𝑢𝐾 (𝐹𝑢) ∈ (𝒫 𝑋 ×t 𝐽))))
115113, 7, 114syl2anc 694 . 2 (𝜑 → (𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 × 𝑌)⟶ 𝐾 ∧ ∀𝑢𝐾 (𝐹𝑢) ∈ (𝒫 𝑋 ×t 𝐽))))
11617, 111, 115mpbir2and 977 1 (𝜑𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  {cab 2637  wral 2941  wrex 2942  {crab 2945  wss 3607  𝒫 cpw 4191  {csn 4210  cop 4216   cuni 4468  cmpt 4762   × cxp 5141  ccnv 5142  dom cdm 5143  cima 5146  Rel wrel 5148   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  Topctop 20746  TopOnctopon 20763   Cn ccn 21076   ×t ctx 21411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-map 7901  df-topgen 16151  df-top 20747  df-topon 20764  df-bases 20798  df-cn 21079  df-tx 21413
This theorem is referenced by:  tgpmulg2  21945
  Copyright terms: Public domain W3C validator