qtoptop2 - Metamath Proof Explorer

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

Theorem qtoptop2 21312

Description: The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.)

**Assertion**
Ref	Expression
qtoptop2	⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝐽 qTop 𝐹) ∈ Top)

Proof of Theorem qtoptop2 Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2610	. . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽
2	1	qtopres 21311	. . 3 ⊢ (𝐹 ∈ 𝑉 → (𝐽 qTop 𝐹) = (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))
3	2	3ad2ant2 1076	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝐽 qTop 𝐹) = (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))
4		simp1 1054	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → 𝐽 ∈ Top)
5		funres 5843	. . . . . . . . . . . . . . 15 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ ∪ 𝐽))
6	5	3ad2ant3 1077	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → Fun (𝐹 ↾ ∪ 𝐽))
7		funforn 6035	. . . . . . . . . . . . . 14 ⊢ (Fun (𝐹 ↾ ∪ 𝐽) ↔ (𝐹 ↾ ∪ 𝐽):dom (𝐹 ↾ ∪ 𝐽)–onto→ran (𝐹 ↾ ∪ 𝐽))
8	6, 7	sylib 207	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝐹 ↾ ∪ 𝐽):dom (𝐹 ↾ ∪ 𝐽)–onto→ran (𝐹 ↾ ∪ 𝐽))
9		dmres 5339	. . . . . . . . . . . . . . 15 ⊢ dom (𝐹 ↾ ∪ 𝐽) = (∪ 𝐽 ∩ dom 𝐹)
10		inss1 3795	. . . . . . . . . . . . . . 15 ⊢ (∪ 𝐽 ∩ dom 𝐹) ⊆ ∪ 𝐽
11	9, 10	eqsstri 3598	. . . . . . . . . . . . . 14 ⊢ dom (𝐹 ↾ ∪ 𝐽) ⊆ ∪ 𝐽
12	11	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → dom (𝐹 ↾ ∪ 𝐽) ⊆ ∪ 𝐽)
13	1	elqtop 21310	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ (𝐹 ↾ ∪ 𝐽):dom (𝐹 ↾ ∪ 𝐽)–onto→ran (𝐹 ↾ ∪ 𝐽) ∧ dom (𝐹 ↾ ∪ 𝐽) ⊆ ∪ 𝐽) → (𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ↔ (𝑦 ⊆ ran (𝐹 ↾ ∪ 𝐽) ∧ (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦) ∈ 𝐽)))
14	4, 8, 12, 13	syl3anc 1318	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ↔ (𝑦 ⊆ ran (𝐹 ↾ ∪ 𝐽) ∧ (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦) ∈ 𝐽)))
15	14	simprbda 651	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ 𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))) → 𝑦 ⊆ ran (𝐹 ↾ ∪ 𝐽))
16		selpw 4115	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝒫 ran (𝐹 ↾ ∪ 𝐽) ↔ 𝑦 ⊆ ran (𝐹 ↾ ∪ 𝐽))
17	15, 16	sylibr 223	. . . . . . . . . 10 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ 𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))) → 𝑦 ∈ 𝒫 ran (𝐹 ↾ ∪ 𝐽))
18	17	ex 449	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) → 𝑦 ∈ 𝒫 ran (𝐹 ↾ ∪ 𝐽)))
19	18	ssrdv 3574	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ⊆ 𝒫 ran (𝐹 ↾ ∪ 𝐽))
20		sstr2 3575	. . . . . . . 8 ⊢ (𝑥 ⊆ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) → ((𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ⊆ 𝒫 ran (𝐹 ↾ ∪ 𝐽) → 𝑥 ⊆ 𝒫 ran (𝐹 ↾ ∪ 𝐽)))
21	19, 20	syl5com 31	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝑥 ⊆ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) → 𝑥 ⊆ 𝒫 ran (𝐹 ↾ ∪ 𝐽)))
22		sspwuni 4547	. . . . . . 7 ⊢ (𝑥 ⊆ 𝒫 ran (𝐹 ↾ ∪ 𝐽) ↔ ∪ 𝑥 ⊆ ran (𝐹 ↾ ∪ 𝐽))
23	21, 22	syl6ib 240	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝑥 ⊆ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) → ∪ 𝑥 ⊆ ran (𝐹 ↾ ∪ 𝐽)))
24		imauni 6408	. . . . . . . 8 ⊢ (^◡(𝐹 ↾ ∪ 𝐽) “ ∪ 𝑥) = ∪ 𝑦 ∈ 𝑥 (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦)
25		simpl1 1057	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ 𝑥 ⊆ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))) → 𝐽 ∈ Top)
26	14	simplbda 652	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ 𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))) → (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦) ∈ 𝐽)
27	26	ralrimiva 2949	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → ∀𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))(^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦) ∈ 𝐽)
28		ssralv 3629	. . . . . . . . . 10 ⊢ (𝑥 ⊆ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) → (∀𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))(^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦) ∈ 𝐽 → ∀𝑦 ∈ 𝑥 (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦) ∈ 𝐽))
29	27, 28	mpan9 485	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ 𝑥 ⊆ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))) → ∀𝑦 ∈ 𝑥 (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦) ∈ 𝐽)
30		iunopn 20528	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝑥 (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦) ∈ 𝐽) → ∪ 𝑦 ∈ 𝑥 (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦) ∈ 𝐽)
31	25, 29, 30	syl2anc 691	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ 𝑥 ⊆ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))) → ∪ 𝑦 ∈ 𝑥 (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦) ∈ 𝐽)
32	24, 31	syl5eqel 2692	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ 𝑥 ⊆ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))) → (^◡(𝐹 ↾ ∪ 𝐽) “ ∪ 𝑥) ∈ 𝐽)
33	32	ex 449	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝑥 ⊆ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) → (^◡(𝐹 ↾ ∪ 𝐽) “ ∪ 𝑥) ∈ 𝐽))
34	23, 33	jcad 554	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝑥 ⊆ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) → (∪ 𝑥 ⊆ ran (𝐹 ↾ ∪ 𝐽) ∧ (^◡(𝐹 ↾ ∪ 𝐽) “ ∪ 𝑥) ∈ 𝐽)))
35	1	elqtop 21310	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ (𝐹 ↾ ∪ 𝐽):dom (𝐹 ↾ ∪ 𝐽)–onto→ran (𝐹 ↾ ∪ 𝐽) ∧ dom (𝐹 ↾ ∪ 𝐽) ⊆ ∪ 𝐽) → (∪ 𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ↔ (∪ 𝑥 ⊆ ran (𝐹 ↾ ∪ 𝐽) ∧ (^◡(𝐹 ↾ ∪ 𝐽) “ ∪ 𝑥) ∈ 𝐽)))
36	4, 8, 12, 35	syl3anc 1318	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (∪ 𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ↔ (∪ 𝑥 ⊆ ran (𝐹 ↾ ∪ 𝐽) ∧ (^◡(𝐹 ↾ ∪ 𝐽) “ ∪ 𝑥) ∈ 𝐽)))
37	34, 36	sylibrd 248	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝑥 ⊆ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) → ∪ 𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))))
38	37	alrimiv 1842	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → ∀𝑥(𝑥 ⊆ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) → ∪ 𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))))
39		inss1 3795	. . . . . 6 ⊢ (𝑥 ∩ 𝑦) ⊆ 𝑥
40	1	elqtop 21310	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ (𝐹 ↾ ∪ 𝐽):dom (𝐹 ↾ ∪ 𝐽)–onto→ran (𝐹 ↾ ∪ 𝐽) ∧ dom (𝐹 ↾ ∪ 𝐽) ⊆ ∪ 𝐽) → (𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ↔ (𝑥 ⊆ ran (𝐹 ↾ ∪ 𝐽) ∧ (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑥) ∈ 𝐽)))
41	4, 8, 12, 40	syl3anc 1318	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ↔ (𝑥 ⊆ ran (𝐹 ↾ ∪ 𝐽) ∧ (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑥) ∈ 𝐽)))
42	41	biimpa 500	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ 𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))) → (𝑥 ⊆ ran (𝐹 ↾ ∪ 𝐽) ∧ (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑥) ∈ 𝐽))
43	42	adantrr 749	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ (𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∧ 𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))) → (𝑥 ⊆ ran (𝐹 ↾ ∪ 𝐽) ∧ (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑥) ∈ 𝐽))
44	43	simpld 474	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ (𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∧ 𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))) → 𝑥 ⊆ ran (𝐹 ↾ ∪ 𝐽))
45	39, 44	syl5ss 3579	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ (𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∧ 𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))) → (𝑥 ∩ 𝑦) ⊆ ran (𝐹 ↾ ∪ 𝐽))
46	6	adantr 480	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ (𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∧ 𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))) → Fun (𝐹 ↾ ∪ 𝐽))
47		inpreima 6250	. . . . . . 7 ⊢ (Fun (𝐹 ↾ ∪ 𝐽) → (^◡(𝐹 ↾ ∪ 𝐽) “ (𝑥 ∩ 𝑦)) = ((^◡(𝐹 ↾ ∪ 𝐽) “ 𝑥) ∩ (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦)))
48	46, 47	syl 17	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ (𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∧ 𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))) → (^◡(𝐹 ↾ ∪ 𝐽) “ (𝑥 ∩ 𝑦)) = ((^◡(𝐹 ↾ ∪ 𝐽) “ 𝑥) ∩ (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦)))
49	4	adantr 480	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ (𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∧ 𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))) → 𝐽 ∈ Top)
50	43	simprd 478	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ (𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∧ 𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))) → (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑥) ∈ 𝐽)
51	26	adantrl 748	. . . . . . 7 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ (𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∧ 𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))) → (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦) ∈ 𝐽)
52		inopn 20529	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑥) ∈ 𝐽 ∧ (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦) ∈ 𝐽) → ((^◡(𝐹 ↾ ∪ 𝐽) “ 𝑥) ∩ (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦)) ∈ 𝐽)
53	49, 50, 51, 52	syl3anc 1318	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ (𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∧ 𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))) → ((^◡(𝐹 ↾ ∪ 𝐽) “ 𝑥) ∩ (^◡(𝐹 ↾ ∪ 𝐽) “ 𝑦)) ∈ 𝐽)
54	48, 53	eqeltrd 2688	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ (𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∧ 𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))) → (^◡(𝐹 ↾ ∪ 𝐽) “ (𝑥 ∩ 𝑦)) ∈ 𝐽)
55	1	elqtop 21310	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ (𝐹 ↾ ∪ 𝐽):dom (𝐹 ↾ ∪ 𝐽)–onto→ran (𝐹 ↾ ∪ 𝐽) ∧ dom (𝐹 ↾ ∪ 𝐽) ⊆ ∪ 𝐽) → ((𝑥 ∩ 𝑦) ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ↔ ((𝑥 ∩ 𝑦) ⊆ ran (𝐹 ↾ ∪ 𝐽) ∧ (^◡(𝐹 ↾ ∪ 𝐽) “ (𝑥 ∩ 𝑦)) ∈ 𝐽)))
56	4, 8, 12, 55	syl3anc 1318	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → ((𝑥 ∩ 𝑦) ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ↔ ((𝑥 ∩ 𝑦) ⊆ ran (𝐹 ↾ ∪ 𝐽) ∧ (^◡(𝐹 ↾ ∪ 𝐽) “ (𝑥 ∩ 𝑦)) ∈ 𝐽)))
57	56	adantr 480	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ (𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∧ 𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))) → ((𝑥 ∩ 𝑦) ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ↔ ((𝑥 ∩ 𝑦) ⊆ ran (𝐹 ↾ ∪ 𝐽) ∧ (^◡(𝐹 ↾ ∪ 𝐽) “ (𝑥 ∩ 𝑦)) ∈ 𝐽)))
58	45, 54, 57	mpbir2and 959	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) ∧ (𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∧ 𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))) → (𝑥 ∩ 𝑦) ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))
59	58	ralrimivva 2954	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → ∀𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))∀𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))(𝑥 ∩ 𝑦) ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))
60		ovex 6577	. . . 4 ⊢ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∈ V
61		istopg 20525	. . . 4 ⊢ ((𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∈ V → ((𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∈ Top ↔ (∀𝑥(𝑥 ⊆ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) → ∪ 𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))) ∧ ∀𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))∀𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))(𝑥 ∩ 𝑦) ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)))))
62	60, 61	ax-mp 5	. . 3 ⊢ ((𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∈ Top ↔ (∀𝑥(𝑥 ⊆ (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) → ∪ 𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))) ∧ ∀𝑥 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))∀𝑦 ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))(𝑥 ∩ 𝑦) ∈ (𝐽 qTop (𝐹 ↾ ∪ 𝐽))))
63	38, 59, 62	sylanbrc 695	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝐽 qTop (𝐹 ↾ ∪ 𝐽)) ∈ Top)
64	3, 63	eqeltrd 2688	1 ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝐽 qTop 𝐹) ∈ Top)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 ∀wal 1473 = wceq 1475 ∈ wcel 1977 ∀wral 2896 Vcvv 3173 ∩ cin 3539 ⊆ wss 3540 𝒫 cpw 4108 ∪ cuni 4372 ∪ ciun 4455 ^◡ccnv 5037 dom cdm 5038 ran crn 5039 ↾ cres 5040 “ cima 5041 Fun wfun 5798 –onto→wfo 5802 (class class class)co 6549 qTop cqtop 15986 Topctop 20517

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-qtop 15990 df-top 20521

This theorem is referenced by: qtoptop 21313

W3C validator