txdis1cn

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)

	Ref	Expression
Hypotheses	txdis1cn.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	txdis1cn.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑌 ) )
	txdis1cn.k	⊢ ( 𝜑 → 𝐾 ∈ Top )
	txdis1cn.f	⊢ ( 𝜑 → 𝐹 Fn ( 𝑋 × 𝑌 ) )
	txdis1cn.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
Assertion	txdis1cn	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝒫 𝑋 ×_t 𝐽 ) Cn 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		txdis1cn.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		txdis1cn.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑌 ) )
3		txdis1cn.k	⊢ ( 𝜑 → 𝐾 ∈ Top )
4		txdis1cn.f	⊢ ( 𝜑 → 𝐹 Fn ( 𝑋 × 𝑌 ) )
5		txdis1cn.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
6	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑌 ) )
7		toptopon2	⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
8	3 7	sylib	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
10		cnf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) : 𝑌 ⟶ ∪ 𝐾 )
11	6 9 5 10	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) : 𝑌 ⟶ ∪ 𝐾 )
12		eqid	⊢ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝐹 𝑦 ) )
13	12	fmpt	⊢ ( ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) ∈ ∪ 𝐾 ↔ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) : 𝑌 ⟶ ∪ 𝐾 )
14	11 13	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) ∈ ∪ 𝐾 )
15	14	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) ∈ ∪ 𝐾 )
16		ffnov	⊢ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝐾 ↔ ( 𝐹 Fn ( 𝑋 × 𝑌 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝐹 𝑦 ) ∈ ∪ 𝐾 ) )
17	4 15 16	sylanbrc	⊢ ( 𝜑 → 𝐹 : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝐾 )
18		cnvimass	⊢ ( ^◡ 𝐹 “ 𝑢 ) ⊆ dom 𝐹
19	4	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) → 𝐹 Fn ( 𝑋 × 𝑌 ) )
20	19	fndmd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) → dom 𝐹 = ( 𝑋 × 𝑌 ) )
21	18 20	sseqtrid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) → ( ^◡ 𝐹 “ 𝑢 ) ⊆ ( 𝑋 × 𝑌 ) )
22		relxp	⊢ Rel ( 𝑋 × 𝑌 )
23		relss	⊢ ( ( ^◡ 𝐹 “ 𝑢 ) ⊆ ( 𝑋 × 𝑌 ) → ( Rel ( 𝑋 × 𝑌 ) → Rel ( ^◡ 𝐹 “ 𝑢 ) ) )
24	21 22 23	mpisyl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) → Rel ( ^◡ 𝐹 “ 𝑢 ) )
25		elpreima	⊢ ( 𝐹 Fn ( 𝑋 × 𝑌 ) → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ^◡ 𝐹 “ 𝑢 ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑧 ⟩ ) ∈ 𝑢 ) ) )
26	19 25	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ^◡ 𝐹 “ 𝑢 ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑧 ⟩ ) ∈ 𝑢 ) ) )
27		opelxp	⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑋 × 𝑌 ) ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) )
28		df-ov	⊢ ( 𝑥 𝐹 𝑧 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑧 ⟩ )
29	28	eqcomi	⊢ ( 𝐹 ‘ ⟨ 𝑥 , 𝑧 ⟩ ) = ( 𝑥 𝐹 𝑧 )
30	29	eleq1i	⊢ ( ( 𝐹 ‘ ⟨ 𝑥 , 𝑧 ⟩ ) ∈ 𝑢 ↔ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 )
31	27 30	anbi12i	⊢ ( ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑧 ⟩ ) ∈ 𝑢 ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) )
32		simprll	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → 𝑥 ∈ 𝑋 )
33		snelpwi	⊢ ( 𝑥 ∈ 𝑋 → { 𝑥 } ∈ 𝒫 𝑋 )
34	32 33	syl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → { 𝑥 } ∈ 𝒫 𝑋 )
35	12	mptpreima	⊢ ( ^◡ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) “ 𝑢 ) = { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 }
36	5	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ) → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
37	36	ad2ant2r	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
38		simplr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → 𝑢 ∈ 𝐾 )
39		cnima	⊢ ( ( ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑢 ∈ 𝐾 ) → ( ^◡ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) “ 𝑢 ) ∈ 𝐽 )
40	37 38 39	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ( ^◡ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝐹 𝑦 ) ) “ 𝑢 ) ∈ 𝐽 )
41	35 40	eqeltrrid	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ∈ 𝐽 )
42		simprlr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → 𝑧 ∈ 𝑌 )
43		simprr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 )
44		vsnid	⊢ 𝑥 ∈ { 𝑥 }
45		opelxp	⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ↔ ( 𝑥 ∈ { 𝑥 } ∧ 𝑧 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) )
46	44 45	mpbiran	⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ↔ 𝑧 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } )
47		oveq2	⊢ ( 𝑦 = 𝑧 → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐹 𝑧 ) )
48	47	eleq1d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 ↔ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) )
49	48	elrab	⊢ ( 𝑧 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ↔ ( 𝑧 ∈ 𝑌 ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) )
50	46 49	bitri	⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ↔ ( 𝑧 ∈ 𝑌 ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) )
51	42 43 50	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) )
52		relxp	⊢ Rel ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } )
53	52	a1i	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → Rel ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) )
54		opelxp	⊢ ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ↔ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) )
55	32	snssd	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → { 𝑥 } ⊆ 𝑋 )
56	55	sselda	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ 𝑛 ∈ { 𝑥 } ) → 𝑛 ∈ 𝑋 )
57	56	adantrr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → 𝑛 ∈ 𝑋 )
58		elrabi	⊢ ( 𝑚 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } → 𝑚 ∈ 𝑌 )
59	58	ad2antll	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → 𝑚 ∈ 𝑌 )
60	57 59	opelxpd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝑋 × 𝑌 ) )
61		df-ov	⊢ ( 𝑛 𝐹 𝑚 ) = ( 𝐹 ‘ ⟨ 𝑛 , 𝑚 ⟩ )
62		elsni	⊢ ( 𝑛 ∈ { 𝑥 } → 𝑛 = 𝑥 )
63	62	ad2antrl	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → 𝑛 = 𝑥 )
64	63	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → ( 𝑛 𝐹 𝑚 ) = ( 𝑥 𝐹 𝑚 ) )
65	61 64	syl5eqr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → ( 𝐹 ‘ ⟨ 𝑛 , 𝑚 ⟩ ) = ( 𝑥 𝐹 𝑚 ) )
66		oveq2	⊢ ( 𝑦 = 𝑚 → ( 𝑥 𝐹 𝑦 ) = ( 𝑥 𝐹 𝑚 ) )
67	66	eleq1d	⊢ ( 𝑦 = 𝑚 → ( ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 ↔ ( 𝑥 𝐹 𝑚 ) ∈ 𝑢 ) )
68	67	elrab	⊢ ( 𝑚 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ↔ ( 𝑚 ∈ 𝑌 ∧ ( 𝑥 𝐹 𝑚 ) ∈ 𝑢 ) )
69	68	simprbi	⊢ ( 𝑚 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } → ( 𝑥 𝐹 𝑚 ) ∈ 𝑢 )
70	69	ad2antll	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → ( 𝑥 𝐹 𝑚 ) ∈ 𝑢 )
71	65 70	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → ( 𝐹 ‘ ⟨ 𝑛 , 𝑚 ⟩ ) ∈ 𝑢 )
72		elpreima	⊢ ( 𝐹 Fn ( 𝑋 × 𝑌 ) → ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( ^◡ 𝐹 “ 𝑢 ) ↔ ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑛 , 𝑚 ⟩ ) ∈ 𝑢 ) ) )
73	4 72	syl	⊢ ( 𝜑 → ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( ^◡ 𝐹 “ 𝑢 ) ↔ ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑛 , 𝑚 ⟩ ) ∈ 𝑢 ) ) )
74	73	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( ^◡ 𝐹 “ 𝑢 ) ↔ ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑛 , 𝑚 ⟩ ) ∈ 𝑢 ) ) )
75	60 71 74	mpbir2and	⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) ∧ ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) → ⟨ 𝑛 , 𝑚 ⟩ ∈ ( ^◡ 𝐹 “ 𝑢 ) )
76	75	ex	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ( ( 𝑛 ∈ { 𝑥 } ∧ 𝑚 ∈ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) → ⟨ 𝑛 , 𝑚 ⟩ ∈ ( ^◡ 𝐹 “ 𝑢 ) ) )
77	54 76	syl5bi	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ( ⟨ 𝑛 , 𝑚 ⟩ ∈ ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) → ⟨ 𝑛 , 𝑚 ⟩ ∈ ( ^◡ 𝐹 “ 𝑢 ) ) )
78	53 77	relssdv	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) )
79		xpeq1	⊢ ( 𝑎 = { 𝑥 } → ( 𝑎 × 𝑏 ) = ( { 𝑥 } × 𝑏 ) )
80	79	eleq2d	⊢ ( 𝑎 = { 𝑥 } → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × 𝑏 ) ) )
81	79	sseq1d	⊢ ( 𝑎 = { 𝑥 } → ( ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ↔ ( { 𝑥 } × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) )
82	80 81	anbi12d	⊢ ( 𝑎 = { 𝑥 } → ( ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × 𝑏 ) ∧ ( { 𝑥 } × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) ) )
83		xpeq2	⊢ ( 𝑏 = { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } → ( { 𝑥 } × 𝑏 ) = ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) )
84	83	eleq2d	⊢ ( 𝑏 = { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × 𝑏 ) ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ) )
85	83	sseq1d	⊢ ( 𝑏 = { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } → ( ( { 𝑥 } × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ↔ ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) )
86	84 85	anbi12d	⊢ ( 𝑏 = { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } → ( ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × 𝑏 ) ∧ ( { 𝑥 } × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ∧ ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) ) )
87	82 86	rspc2ev	⊢ ( ( { 𝑥 } ∈ 𝒫 𝑋 ∧ { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ∈ 𝐽 ∧ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ∧ ( { 𝑥 } × { 𝑦 ∈ 𝑌 ∣ ( 𝑥 𝐹 𝑦 ) ∈ 𝑢 } ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) ) → ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) )
88	34 41 51 78 87	syl112anc	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) )
89		opex	⊢ ⟨ 𝑥 , 𝑧 ⟩ ∈ V
90		eleq1	⊢ ( 𝑣 = ⟨ 𝑥 , 𝑧 ⟩ → ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ) )
91	90	anbi1d	⊢ ( 𝑣 = ⟨ 𝑥 , 𝑧 ⟩ → ( ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) ↔ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) ) )
92	91	2rexbidv	⊢ ( 𝑣 = ⟨ 𝑥 , 𝑧 ⟩ → ( ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) ↔ ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) ) )
93	89 92	elab	⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ { 𝑣 ∣ ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) } ↔ ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) )
94	88 93	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ { 𝑣 ∣ ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) } )
95	94	ex	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) → ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) ∧ ( 𝑥 𝐹 𝑧 ) ∈ 𝑢 ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ { 𝑣 ∣ ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) } ) )
96	31 95	syl5bi	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) → ( ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 ‘ ⟨ 𝑥 , 𝑧 ⟩ ) ∈ 𝑢 ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ { 𝑣 ∣ ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) } ) )
97	26 96	sylbid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) → ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( ^◡ 𝐹 “ 𝑢 ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ { 𝑣 ∣ ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) } ) )
98	24 97	relssdv	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) → ( ^◡ 𝐹 “ 𝑢 ) ⊆ { 𝑣 ∣ ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) } )
99		ssabral	⊢ ( ( ^◡ 𝐹 “ 𝑢 ) ⊆ { 𝑣 ∣ ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) } ↔ ∀ 𝑣 ∈ ( ^◡ 𝐹 “ 𝑢 ) ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) )
100	98 99	sylib	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) → ∀ 𝑣 ∈ ( ^◡ 𝐹 “ 𝑢 ) ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) )
101		distopon	⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ ( TopOn ‘ 𝑋 ) )
102	1 101	syl	⊢ ( 𝜑 → 𝒫 𝑋 ∈ ( TopOn ‘ 𝑋 ) )
103	102	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) → 𝒫 𝑋 ∈ ( TopOn ‘ 𝑋 ) )
104	2	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) → 𝐽 ∈ ( TopOn ‘ 𝑌 ) )
105		eltx	⊢ ( ( 𝒫 𝑋 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( ^◡ 𝐹 “ 𝑢 ) ∈ ( 𝒫 𝑋 ×_t 𝐽 ) ↔ ∀ 𝑣 ∈ ( ^◡ 𝐹 “ 𝑢 ) ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) ) )
106	103 104 105	syl2anc	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) → ( ( ^◡ 𝐹 “ 𝑢 ) ∈ ( 𝒫 𝑋 ×_t 𝐽 ) ↔ ∀ 𝑣 ∈ ( ^◡ 𝐹 “ 𝑢 ) ∃ 𝑎 ∈ 𝒫 𝑋 ∃ 𝑏 ∈ 𝐽 ( 𝑣 ∈ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( ^◡ 𝐹 “ 𝑢 ) ) ) )
107	100 106	mpbird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐾 ) → ( ^◡ 𝐹 “ 𝑢 ) ∈ ( 𝒫 𝑋 ×_t 𝐽 ) )
108	107	ralrimiva	⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐾 ( ^◡ 𝐹 “ 𝑢 ) ∈ ( 𝒫 𝑋 ×_t 𝐽 ) )
109		txtopon	⊢ ( ( 𝒫 𝑋 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝒫 𝑋 ×_t 𝐽 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
110	102 2 109	syl2anc	⊢ ( 𝜑 → ( 𝒫 𝑋 ×_t 𝐽 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
111		iscn	⊢ ( ( ( 𝒫 𝑋 ×_t 𝐽 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ) → ( 𝐹 ∈ ( ( 𝒫 𝑋 ×_t 𝐽 ) Cn 𝐾 ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝐾 ∧ ∀ 𝑢 ∈ 𝐾 ( ^◡ 𝐹 “ 𝑢 ) ∈ ( 𝒫 𝑋 ×_t 𝐽 ) ) ) )
112	110 8 111	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝒫 𝑋 ×_t 𝐽 ) Cn 𝐾 ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝐾 ∧ ∀ 𝑢 ∈ 𝐾 ( ^◡ 𝐹 “ 𝑢 ) ∈ ( 𝒫 𝑋 ×_t 𝐽 ) ) ) )
113	17 108 112	mpbir2and	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝒫 𝑋 ×_t 𝐽 ) Cn 𝐾 ) )

Metamath Proof Explorer

Theorem txdis1cn

Proof