Theorem txdis1cn 23916

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 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐽 ∈ (TopOn‘𝑌))
4		txdis1cn.k	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ Top)
5		toptopon2 23198	. . . . . . . 8 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾))
6	4, 5	sylib 221	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘∪ 𝐾))
7	6	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘∪ 𝐾))
8		txdis1cn.1	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
9		cnf2 23529	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑌) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾) ∧ (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)):𝑌⟶∪ 𝐾)
10	3, 7, 8, 9	syl3anc 1398	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)):𝑌⟶∪ 𝐾)
11		eqid 2760	. . . . . 6 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) = (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦))
12	11	fmpt 7098	. . . . 5 ⊢ (∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾 ↔ (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)):𝑌⟶∪ 𝐾)
13	10, 12	sylibr 237	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾)
14	13	ralrimiva 3154	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾)
15		ffnov 7534	. . 3 ⊢ (𝐹:(𝑋 × 𝑌)⟶∪ 𝐾 ↔ (𝐹 Fn (𝑋 × 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝐹𝑦) ∈ ∪ 𝐾))
16	1, 14, 15	sylanbrc 595	. 2 ⊢ (𝜑 → 𝐹:(𝑋 × 𝑌)⟶∪ 𝐾)
17		cnvimass 6072	. . . . . . . 8 ⊢ (◡𝐹 “ 𝑢) ⊆ dom 𝐹
18	1	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → 𝐹 Fn (𝑋 × 𝑌))
19	18	fndmd 6632	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → dom 𝐹 = (𝑋 × 𝑌))
20	17, 19	sseqtrid 3972	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (◡𝐹 “ 𝑢) ⊆ (𝑋 × 𝑌))
21		relxp 5665	. . . . . . 7 ⊢ Rel (𝑋 × 𝑌)
22		relss 5754	. . . . . . 7 ⊢ ((◡𝐹 “ 𝑢) ⊆ (𝑋 × 𝑌) → (Rel (𝑋 × 𝑌) → Rel (◡𝐹 “ 𝑢)))
23	20, 21, 22	mpisyl 22	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → Rel (◡𝐹 “ 𝑢))
24		elpreima 7045	. . . . . . . 8 ⊢ (𝐹 Fn (𝑋 × 𝑌) → (⟨𝑥, 𝑧⟩ ∈ (◡𝐹 “ 𝑢) ↔ (⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢)))
25	18, 24	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (⟨𝑥, 𝑧⟩ ∈ (◡𝐹 “ 𝑢) ↔ (⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢)))
26		opelxp 5683	. . . . . . . . 9 ⊢ (⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ↔ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌))
27		df-ov 7411	. . . . . . . . . . 11 ⊢ (𝑥𝐹𝑧) = (𝐹‘⟨𝑥, 𝑧⟩)
28	27	eqcomi 2769	. . . . . . . . . 10 ⊢ (𝐹‘⟨𝑥, 𝑧⟩) = (𝑥𝐹𝑧)
29	28	eleq1i 2851	. . . . . . . . 9 ⊢ ((𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢 ↔ (𝑥𝐹𝑧) ∈ 𝑢)
30	26, 29	anbi12i 640	. . . . . . . 8 ⊢ ((⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢))
31		simprll 791	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑥 ∈ 𝑋)
32		snelpwi 5411	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑋 → {𝑥} ∈ 𝒫 𝑋)
33	31, 32	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑥} ∈ 𝒫 𝑋)
34	11	mptpreima 6228	. . . . . . . . . . . 12 ⊢ (◡(𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}
35	8	adantrr 730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
36	35	ad2ant2r 760	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾))
37		simplr 781	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑢 ∈ 𝐾)
38		cnima 23545	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾) ∧ 𝑢 ∈ 𝐾) → (◡(𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) ∈ 𝐽)
39	36, 37, 38	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (◡(𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) “ 𝑢) ∈ 𝐽)
40	34, 39	eqeltrrid 2865	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ∈ 𝐽)
41		simprlr 792	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → 𝑧 ∈ 𝑌)
42		simprr 785	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (𝑥𝐹𝑧) ∈ 𝑢)
43		vsnid 4623	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ {𝑥}
44		opelxp 5683	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑥 ∈ {𝑥} ∧ 𝑧 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
45	43, 44	mpbiran 722	. . . . . . . . . . . . 13 ⊢ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ 𝑧 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})
46		oveq2 7416	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑧 → (𝑥𝐹𝑦) = (𝑥𝐹𝑧))
47	46	eleq1d 2845	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑧 → ((𝑥𝐹𝑦) ∈ 𝑢 ↔ (𝑥𝐹𝑧) ∈ 𝑢))
48	47	elrab 3644	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ↔ (𝑧 ∈ 𝑌 ∧ (𝑥𝐹𝑧) ∈ 𝑢))
49	45, 48	bitri 278	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑧 ∈ 𝑌 ∧ (𝑥𝐹𝑧) ∈ 𝑢))
50	41, 42, 49	sylanbrc 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
51		relxp 5665	. . . . . . . . . . . . 13 ⊢ Rel ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})
52	51	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → Rel ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
53		opelxp 5683	. . . . . . . . . . . . 13 ⊢ (⟨𝑛, 𝑚⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ↔ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
54	31	snssd 4746	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → {𝑥} ⊆ 𝑋)
55	54	sselda 3930	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ 𝑛 ∈ {𝑥}) → 𝑛 ∈ 𝑋)
56	55	adantrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑛 ∈ 𝑋)
57		elrabi 3640	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → 𝑚 ∈ 𝑌)
58	57	ad2antll 742	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑚 ∈ 𝑌)
59	56, 58	opelxpd 5686	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → ⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌))
60		df-ov 7411	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛𝐹𝑚) = (𝐹‘⟨𝑛, 𝑚⟩)
61		elsni 4600	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ {𝑥} → 𝑛 = 𝑥)
62	61	ad2antrl 741	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → 𝑛 = 𝑥)
63	62	oveq1d 7423	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝑛𝐹𝑚) = (𝑥𝐹𝑚))
64	60, 63	eqtr3id 2809	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝐹‘⟨𝑛, 𝑚⟩) = (𝑥𝐹𝑚))
65		oveq2 7416	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑚 → (𝑥𝐹𝑦) = (𝑥𝐹𝑚))
66	65	eleq1d 2845	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑚 → ((𝑥𝐹𝑦) ∈ 𝑢 ↔ (𝑥𝐹𝑚) ∈ 𝑢))
67	66	elrab 3644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ↔ (𝑚 ∈ 𝑌 ∧ (𝑥𝐹𝑚) ∈ 𝑢))
68	67	simprbi 503	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (𝑥𝐹𝑚) ∈ 𝑢)
69	68	ad2antll 742	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝑥𝐹𝑚) ∈ 𝑢)
70	64, 69	eqeltrd 2860	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)
71		elpreima 7045	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn (𝑋 × 𝑌) → (⟨𝑛, 𝑚⟩ ∈ (◡𝐹 “ 𝑢) ↔ (⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)))
72	1, 71	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⟨𝑛, 𝑚⟩ ∈ (◡𝐹 “ 𝑢) ↔ (⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)))
73	72	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → (⟨𝑛, 𝑚⟩ ∈ (◡𝐹 “ 𝑢) ↔ (⟨𝑛, 𝑚⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑛, 𝑚⟩) ∈ 𝑢)))
74	59, 70, 73	mpbir2and 726	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) ∧ (𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})) → ⟨𝑛, 𝑚⟩ ∈ (◡𝐹 “ 𝑢))
75	74	ex 418	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ((𝑛 ∈ {𝑥} ∧ 𝑚 ∈ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) → ⟨𝑛, 𝑚⟩ ∈ (◡𝐹 “ 𝑢)))
76	53, 75	biimtrid 245	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → (⟨𝑛, 𝑚⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) → ⟨𝑛, 𝑚⟩ ∈ (◡𝐹 “ 𝑢)))
77	52, 76	relssdv 5760	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢))
78		xpeq1 5661	. . . . . . . . . . . . . 14 ⊢ (𝑎 = {𝑥} → (𝑎 × 𝑏) = ({𝑥} × 𝑏))
79	78	eleq2d 2846	. . . . . . . . . . . . 13 ⊢ (𝑎 = {𝑥} → (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ↔ ⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏)))
80	78	sseq1d 3961	. . . . . . . . . . . . 13 ⊢ (𝑎 = {𝑥} → ((𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢) ↔ ({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢)))
81	79, 80	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑎 = {𝑥} → ((⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏) ∧ ({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢))))
82		xpeq2 5668	. . . . . . . . . . . . . 14 ⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → ({𝑥} × 𝑏) = ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}))
83	82	eleq2d 2846	. . . . . . . . . . . . 13 ⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏) ↔ ⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢})))
84	82	sseq1d 3961	. . . . . . . . . . . . 13 ⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → (({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢) ↔ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢)))
85	83, 84	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑏 = {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} → ((⟨𝑥, 𝑧⟩ ∈ ({𝑥} × 𝑏) ∧ ({𝑥} × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ∧ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢))))
86	81, 85	rspc2ev 3588	. . . . . . . . . . 11 ⊢ (({𝑥} ∈ 𝒫 𝑋 ∧ {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢} ∈ 𝐽 ∧ (⟨𝑥, 𝑧⟩ ∈ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ∧ ({𝑥} × {𝑦 ∈ 𝑌 ∣ (𝑥𝐹𝑦) ∈ 𝑢}) ⊆ (◡𝐹 “ 𝑢))) → ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))
87	33, 40, 50, 77, 86	syl112anc 1401	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))
88		opex 5431	. . . . . . . . . . 11 ⊢ ⟨𝑥, 𝑧⟩ ∈ V
89		eleq1 2848	. . . . . . . . . . . . 13 ⊢ (𝑣 = ⟨𝑥, 𝑧⟩ → (𝑣 ∈ (𝑎 × 𝑏) ↔ ⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏)))
90	89	anbi1d 643	. . . . . . . . . . . 12 ⊢ (𝑣 = ⟨𝑥, 𝑧⟩ → ((𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))))
91	90	2rexbidv 3227	. . . . . . . . . . 11 ⊢ (𝑣 = ⟨𝑥, 𝑧⟩ → (∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)) ↔ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))))
92	88, 91	elab 3632	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))} ↔ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (⟨𝑥, 𝑧⟩ ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))
93	87, 92	sylibr 237	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑢 ∈ 𝐾) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢)) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))})
94	93	ex 418	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (((𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌) ∧ (𝑥𝐹𝑧) ∈ 𝑢) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))}))
95	30, 94	biimtrid 245	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → ((⟨𝑥, 𝑧⟩ ∈ (𝑋 × 𝑌) ∧ (𝐹‘⟨𝑥, 𝑧⟩) ∈ 𝑢) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))}))
96	25, 95	sylbid 243	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (⟨𝑥, 𝑧⟩ ∈ (◡𝐹 “ 𝑢) → ⟨𝑥, 𝑧⟩ ∈ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))}))
97	23, 96	relssdv 5760	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (◡𝐹 “ 𝑢) ⊆ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))})
98		ssabral 4011	. . . . 5 ⊢ ((◡𝐹 “ 𝑢) ⊆ {𝑣 ∣ ∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))} ↔ ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))
99	97, 98	sylib 221	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢)))
100		txdis1cn.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
101		distopon 23277	. . . . . . 7 ⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ (TopOn‘𝑋))
102	100, 101	syl 18	. . . . . 6 ⊢ (𝜑 → 𝒫 𝑋 ∈ (TopOn‘𝑋))
103	102	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → 𝒫 𝑋 ∈ (TopOn‘𝑋))
104	2	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → 𝐽 ∈ (TopOn‘𝑌))
105		eltx 23849	. . . . 5 ⊢ ((𝒫 𝑋 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑌)) → ((◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽) ↔ ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))))
106	103, 104, 105	syl2anc 596	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → ((◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽) ↔ ∀𝑣 ∈ (◡𝐹 “ 𝑢)∃𝑎 ∈ 𝒫 𝑋∃𝑏 ∈ 𝐽 (𝑣 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐹 “ 𝑢))))
107	99, 106	mpbird 260	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ 𝐾) → (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽))
108	107	ralrimiva 3154	. 2 ⊢ (𝜑 → ∀𝑢 ∈ 𝐾 (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽))
109		txtopon 23872	. . . 4 ⊢ ((𝒫 𝑋 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ (TopOn‘𝑌)) → (𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌)))
110	102, 2, 109	syl2anc 596	. . 3 ⊢ (𝜑 → (𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌)))
111		iscn 23515	. . 3 ⊢ (((𝒫 𝑋 ×t 𝐽) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐾 ∈ (TopOn‘∪ 𝐾)) → (𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 × 𝑌)⟶∪ 𝐾 ∧ ∀𝑢 ∈ 𝐾 (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽))))
112	110, 6, 111	syl2anc 596	. 2 ⊢ (𝜑 → (𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾) ↔ (𝐹:(𝑋 × 𝑌)⟶∪ 𝐾 ∧ ∀𝑢 ∈ 𝐾 (◡𝐹 “ 𝑢) ∈ (𝒫 𝑋 ×t 𝐽))))
113	16, 108, 112	mpbir2and 726	1 ⊢ (𝜑 → 𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {cab 2738  ∀wral 3076  ∃wrex 3086  {crab 3412   ⊆ wss 3898  𝒫 cpw 4556  {csn 4583  ⟨cop 4589  ∪ cuni 4866   ↦ cmpt 5185   × cxp 5645  ^◡ccnv 5646  dom cdm 5647   “ cima 5650  Rel wrel 5652   Fn wfn 6522  ⟶wf 6523  ‘cfv 6527  (class class class)co 7408  Topctop 23173  TopOnctopon 23190   Cn ccn 23504   ×_t ctx 23841

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-fv 6535  df-ov 7411  df-oprab 7412  df-mpo 7413  df-1st 7984  df-2nd 7985  df-map 8827  df-topgen 17576  df-top 23174  df-topon 23191  df-bases 23226  df-cn 23507  df-tx 23843

This theorem is used by:  tgpmulg2  24375