Theorem txdis1cn 21851

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.

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 𝐾))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601   ∈ wcel 2107  {cab 2763  ∀wral 3090  ∃wrex 3091  {crab 3094   ⊆ wss 3792  𝒫 cpw 4379  {csn 4398  ⟨cop 4404  ∪ cuni 4673   ↦ cmpt 4967   × cxp 5355  ^◡ccnv 5356  dom cdm 5357   “ cima 5360  Rel wrel 5362   Fn wfn 6132  ⟶wf 6133  ‘cfv 6137  (class class class)co 6924  Topctop 21109  TopOnctopon 21126   Cn ccn 21440   ×_t ctx 21776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-fv 6145  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-1st 7447  df-2nd 7448  df-map 8144  df-topgen 16494  df-top 21110  df-topon 21127  df-bases 21162  df-cn 21443  df-tx 21778

This theorem is referenced by:  tgpmulg2  22310