Theorem txdis1cn 12918

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 274	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑌))
4		txdis1cn.k	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ Top)
5		toptopon2 12657	. . . . . . . 8 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾))
6	4, 5	sylib 121	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾))
7	6	adantr 274	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘∪ 𝐾))
8		txdis1cn.1	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
9		cnf2 12845	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾) ∧ (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)):𝑌⟶∪ 𝐾)
10	3, 7, 8, 9	syl3anc 1228	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)):𝑌⟶∪ 𝐾)
11		eqid 2165	. . . . . 6 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) = (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦))
12	11	fmpt 5635	. . . . 5 ⊢ (∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾 ↔ (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)):𝑌⟶∪ 𝐾)
13	10, 12	sylibr 133	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾)
14	13	ralrimiva 2539	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾)
15		ffnov 5946	. . 3 ⊢ (𝐹:(𝑋 × 𝑌)⟶∪ 𝐾 ↔ (𝐹 Fn (𝑋 × 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾))
16	1, 14, 15	sylanbrc 414	. 2 ⊢ (𝜑 → 𝐹:(𝑋 × 𝑌)⟶∪ 𝐾)
17		cnvimass 4967	. . . . . . . 8 ⊢ (◡𝐹 “ 𝑢) ⊆ dom 𝐹
18	1	adantr 274	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → 𝐹 Fn (𝑋 × 𝑌))
19		fndm 5287	. . . . . . . . 9 ⊢ (𝐹 Fn (𝑋 × 𝑌) → dom 𝐹 = (𝑋 × 𝑌))
20	18, 19	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → dom 𝐹 = (𝑋 × 𝑌))
21	17, 20	sseqtrid 3192	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (◡𝐹 “ 𝑢) ⊆ (𝑋 × 𝑌))
22		relxp 4713	. . . . . . 7 ⊢ Rel (𝑋 × 𝑌)
23		relss 4691	. . . . . . 7 ⊢ ((◡𝐹 “ 𝑢) ⊆ (𝑋 × 𝑌) → (Rel (𝑋 × 𝑌) → Rel (◡𝐹 “ 𝑢)))
24	21, 22, 23	mpisyl 1434	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → Rel (◡𝐹 “ 𝑢))
25		elpreima 5604	. . . . . . . 8 ⊢ (𝐹 Fn (𝑋 × 𝑌) → (⟨𝑥, 𝑧⟩ ∈ (◡𝐹 “ 𝑢) ↔ (⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢)))
26	18, 25	syl 14	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (⟨𝑥, 𝑧⟩ ∈ (◡𝐹 “ 𝑢) ↔ (⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢)))
27		opelxp 4634	. . . . . . . . 9 ⊢ (⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ↔ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌))
28		df-ov 5845	. . . . . . . . . . 11 ⊢ (𝑥𝐹𝑧) = (𝐹‘⟨𝑥, 𝑧⟩)
29	28	eqcomi 2169	. . . . . . . . . 10 ⊢ (𝐹‘⟨𝑥, 𝑧⟩) = (𝑥𝐹𝑧)
30	29	eleq1i 2232	. . . . . . . . 9 ⊢ ((𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢 ↔ (𝑥𝐹𝑧) ∈ 𝑢)
31	27, 30	anbi12i 456	. . . . . . . 8 ⊢ ((⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢))
32		simprll 527	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑥 ∈ 𝑋)
33		snelpwi 4190	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑋 → {𝑥} ∈ 𝒫 𝑋)
34	32, 33	syl 14	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑥} ∈ 𝒫 𝑋)
35	11	mptpreima 5097	. . . . . . . . . . . 12 ⊢ (◡(𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}
36	8	adantrr 471	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
37	36	ad2ant2r 501	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
38		simplr 520	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑢 ∈ 𝐾)
39		cnima 12860	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾) ∧ 𝑢 ∈ 𝐾) → (◡(𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) ∈ 𝐽)
40	37, 38, 39	syl2anc 409	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (◡(𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) ∈ 𝐽)
41	35, 40	eqeltrrid 2254	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ∈ 𝐽)
42		simprlr 528	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑧 ∈ 𝑌)
43		simprr 522	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (𝑥𝐹𝑧) ∈ 𝑢)
44		vsnid 3608	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ {𝑥}
45		opelxp 4634	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑥 ∈ {𝑥} ∧ 𝑧 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
46	44, 45	mpbiran 930	. . . . . . . . . . . . 13 ⊢ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ 𝑧 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})
47		oveq2 5850	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → (𝑥𝐹𝑦) = (𝑥𝐹𝑧))
48	47	eleq1d 2235	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → ((𝑥𝐹𝑦) ∈ 𝑢 ↔ (𝑥𝐹𝑧) ∈ 𝑢))
49	48	elrab 2882	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ↔ (𝑧 ∈ 𝑌 ∧ (𝑥𝐹𝑧) ∈ 𝑢))
50	46, 49	bitri 183	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑧 ∈ 𝑌 ∧ (𝑥𝐹𝑧) ∈ 𝑢))
51	42, 43, 50	sylanbrc 414	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
52		relxp 4713	. . . . . . . . . . . . 13 ⊢ Rel ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})
53	52	a1i 9	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → Rel ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
54		opelxp 4634	. . . . . . . . . . . . 13 ⊢ (⟨𝑛, 𝑚⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
55	32	snssd 3718	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑥} ⊆ 𝑋)
56	55	sselda 3142	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ 𝑛 ∈ {𝑥}) → 𝑛 ∈ 𝑋)
57	56	adantrr 471	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑛 ∈ 𝑋)
58		elrabi 2879	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → 𝑚 ∈ 𝑌)
59	58	ad2antll 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑚 ∈ 𝑌)
60	57, 59	opelxpd 4637	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → ⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌))
61		df-ov 5845	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛𝐹𝑚) = (𝐹‘⟨𝑛, 𝑚⟩)
62		elsni 3594	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ {𝑥} → 𝑛 = 𝑥)
63	62	ad2antrl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑛 = 𝑥)
64	63	oveq1d 5857	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝑛𝐹𝑚) = (𝑥𝐹𝑚))
65	61, 64	eqtr3id 2213	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝐹‘⟨𝑛, 𝑚⟩) = (𝑥𝐹𝑚))
66		oveq2 5850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑚 → (𝑥𝐹𝑦) = (𝑥𝐹𝑚))
67	66	eleq1d 2235	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑚 → ((𝑥𝐹𝑦) ∈ 𝑢 ↔ (𝑥𝐹𝑚) ∈ 𝑢))
68	67	elrab 2882	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ↔ (𝑚 ∈ 𝑌 ∧ (𝑥𝐹𝑚) ∈ 𝑢))
69	68	simprbi 273	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (𝑥𝐹𝑚) ∈ 𝑢)
70	69	ad2antll 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝑥𝐹𝑚) ∈ 𝑢)
71	65, 70	eqeltrd 2243	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)
72		elpreima 5604	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn (𝑋 × 𝑌) → (⟨𝑛, 𝑚⟩ ∈ (◡𝐹 “ 𝑢) ↔ (⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)))
73	1, 72	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⟨𝑛, 𝑚⟩ ∈ (◡𝐹 “ 𝑢) ↔ (⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)))
74	73	ad3antrrr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (⟨𝑛, 𝑚⟩ ∈ (◡𝐹 “ 𝑢) ↔ (⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)))
75	60, 71, 74	mpbir2and 934	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → ⟨𝑛, 𝑚⟩ ∈ (◡𝐹 “ 𝑢))
76	75	ex 114	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ((𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) → ⟨𝑛, 𝑚⟩ ∈ (◡𝐹 “ 𝑢)))
77	54, 76	syl5bi 151	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (⟨𝑛, 𝑚⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) → ⟨𝑛, 𝑚⟩ ∈ (◡𝐹 “ 𝑢)))
78	53, 77	relssdv 4696	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢))
79		xpeq1 4618	. . . . . . . . . . . . . 14 ⊢ (𝑎 = {𝑥} → (𝑎 × 𝑏) = ({𝑥} × 𝑏))
80	79	eleq2d 2236	. . . . . . . . . . . . 13 ⊢ (𝑎 = {𝑥} → (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ↔ ⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏)))
81	79	sseq1d 3171	. . . . . . . . . . . . 13 ⊢ (𝑎 = {𝑥} → ((𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢) ↔ ({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢)))
82	80, 81	anbi12d 465	. . . . . . . . . . . 12 ⊢ (𝑎 = {𝑥} → ((⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏) ∧ ({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢))))
83		xpeq2 4619	. . . . . . . . . . . . . 14 ⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → ({𝑥} × 𝑏) = ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
84	83	eleq2d 2236	. . . . . . . . . . . . 13 ⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏) ↔ ⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})))
85	83	sseq1d 3171	. . . . . . . . . . . . 13 ⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢) ↔ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢)))
86	84, 85	anbi12d 465	. . . . . . . . . . . 12 ⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → ((⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏) ∧ ({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ∧ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢))))
87	82, 86	rspc2ev 2845	. . . . . . . . . . 11 ⊢ (({𝑥} ∈ 𝒫 𝑋 ∧ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ∈ 𝐽 ∧ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ∧ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢))) → ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))
88	34, 41, 51, 78, 87	syl112anc 1232	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))
89		vex 2729	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
90		vex 2729	. . . . . . . . . . . 12 ⊢ 𝑧 ∈ V
91	89, 90	opex 4207	. . . . . . . . . . 11 ⊢ ⟨𝑥, 𝑧⟩ ∈ V
92		eleq1 2229	. . . . . . . . . . . . 13 ⊢ (𝑣 = ⟨𝑥, 𝑧⟩ → (𝑣 ∈ (𝑎 × 𝑏) ↔ ⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏)))
93	92	anbi1d 461	. . . . . . . . . . . 12 ⊢ (𝑣 = ⟨𝑥, 𝑧⟩ → ((𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))))
94	93	2rexbidv 2491	. . . . . . . . . . 11 ⊢ (𝑣 = ⟨𝑥, 𝑧⟩ → (∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))))
95	91, 94	elab 2870	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))} ↔ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))
96	88, 95	sylibr 133	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))})
97	96	ex 114	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))}))
98	31, 97	syl5bi 151	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → ((⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))}))
99	26, 98	sylbid 149	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (⟨𝑥, 𝑧⟩ ∈ (◡𝐹 “ 𝑢) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))}))
100	24, 99	relssdv 4696	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (◡𝐹 “ 𝑢) ⊆ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))})
101		ssabral 3213	. . . . 5 ⊢ ((◡𝐹 “ 𝑢) ⊆ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))} ↔ ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))
102	100, 101	sylib 121	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))
103		txdis1cn.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
104		distopon 12727	. . . . . . 7 ⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ (TopOn‘𝑋))
105	103, 104	syl 14	. . . . . 6 ⊢ (𝜑 → 𝒫 𝑋 ∈ (TopOn‘𝑋))
106	105	adantr 274	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → 𝒫 𝑋 ∈ (TopOn‘𝑋))
107	2	adantr 274	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → 𝐽 ∈ (TopOn‘𝑌))
108		eltx 12899	. . . . 5 ⊢ ((𝒫 𝑋 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑌)) → ((◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽) ↔ ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))))
109	106, 107, 108	syl2anc 409	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → ((◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽) ↔ ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))))
110	102, 109	mpbird 166	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽))
111	110	ralrimiva 2539	. 2 ⊢ (𝜑 → ∀𝑢 ∈ 𝐾 (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽))
112		txtopon 12902	. . . 4 ⊢ ((𝒫 𝑋 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑌)) → (𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌)))
113	105, 2, 112	syl2anc 409	. . 3 ⊢ (𝜑 → (𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌)))
114		iscn 12837	. . 3 ⊢ (((𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)) → (𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 × 𝑌)⟶∪ 𝐾 ∧ ∀𝑢 ∈ 𝐾 (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽))))
115	113, 6, 114	syl2anc 409	. 2 ⊢ (𝜑 → (𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 × 𝑌)⟶∪ 𝐾 ∧ ∀𝑢 ∈ 𝐾 (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽))))
116	16, 111, 115	mpbir2and 934	1 ⊢ (𝜑 → 𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1343   ∈ wcel 2136  {cab 2151  ∀wral 2444  ∃wrex 2445  {crab 2448   ⊆ wss 3116  𝒫 cpw 3559  {csn 3576  ⟨cop 3579  ∪ cuni 3789   ↦ cmpt 4043   × cxp 4602  ^◡ccnv 4603  dom cdm 4604   “ cima 4607  Rel wrel 4609   Fn wfn 5183  ⟶wf 5184  ‘cfv 5188  (class class class)co 5842  Topctop 12635  TopOnctopon 12648   Cn ccn 12825   ×_t ctx 12892

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-13 2138  ax-14 2139  ax-ext 2147  ax-coll 4097  ax-sep 4100  ax-pow 4153  ax-pr 4187  ax-un 4411  ax-setind 4514

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-fal 1349  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ne 2337  df-ral 2449  df-rex 2450  df-reu 2451  df-rab 2453  df-v 2728  df-sbc 2952  df-csb 3046  df-dif 3118  df-un 3120  df-in 3122  df-ss 3129  df-pw 3561  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-iun 3868  df-br 3983  df-opab 4044  df-mpt 4045  df-id 4271  df-xp 4610  df-rel 4611  df-cnv 4612  df-co 4613  df-dm 4614  df-rn 4615  df-res 4616  df-ima 4617  df-iota 5153  df-fun 5190  df-fn 5191  df-f 5192  df-f1 5193  df-fo 5194  df-f1o 5195  df-fv 5196  df-ov 5845  df-oprab 5846  df-mpo 5847  df-1st 6108  df-2nd 6109  df-map 6616  df-topgen 12577  df-top 12636  df-topon 12649  df-bases 12681  df-cn 12828  df-tx 12893

This theorem is referenced by: (None)