This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qtoptop2

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

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

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 1 qtopres ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐽 qTop 𝐹 ) = ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) )
3 2 3ad2ant2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( 𝐽 qTop 𝐹 ) = ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) )
4 simp1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → 𝐽 ∈ Top )
5 funres ⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ ∪ 𝐽 ) )
6 5 3ad2ant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → Fun ( 𝐹 ↾ ∪ 𝐽 ) )
7 funforn ⊢ ( Fun ( 𝐹 ↾ ∪ 𝐽 ) ↔ ( 𝐹 ↾ ∪ 𝐽 ) : dom ( 𝐹 ↾ ∪ 𝐽 ) –onto→ ran ( 𝐹 ↾ ∪ 𝐽 ) )
8 6 7 sylib ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( 𝐹 ↾ ∪ 𝐽 ) : dom ( 𝐹 ↾ ∪ 𝐽 ) –onto→ ran ( 𝐹 ↾ ∪ 𝐽 ) )
9 dmres ⊢ dom ( 𝐹 ↾ ∪ 𝐽 ) = ( ∪ 𝐽 ∩ dom 𝐹 )
10 inss1 ⊢ ( ∪ 𝐽 ∩ dom 𝐹 ) ⊆ ∪ 𝐽
11 9 10 eqsstri ⊢ dom ( 𝐹 ↾ ∪ 𝐽 ) ⊆ ∪ 𝐽
12 11 a1i ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → dom ( 𝐹 ↾ ∪ 𝐽 ) ⊆ ∪ 𝐽 )
13 1 elqtop ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐹 ↾ ∪ 𝐽 ) : dom ( 𝐹 ↾ ∪ 𝐽 ) –onto→ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ dom ( 𝐹 ↾ ∪ 𝐽 ) ⊆ ∪ 𝐽 ) → ( 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ↔ ( 𝑦 ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ∈ 𝐽 ) ) )
14 4 8 12 13 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ↔ ( 𝑦 ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ∈ 𝐽 ) ) )
15 14 simprbda ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) → 𝑦 ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) )
16 velpw ⊢ ( 𝑦 ∈ 𝒫 ran ( 𝐹 ↾ ∪ 𝐽 ) ↔ 𝑦 ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) )
17 15 16 sylibr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) → 𝑦 ∈ 𝒫 ran ( 𝐹 ↾ ∪ 𝐽 ) )
18 17 ex ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) → 𝑦 ∈ 𝒫 ran ( 𝐹 ↾ ∪ 𝐽 ) ) )
19 18 ssrdv ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ⊆ 𝒫 ran ( 𝐹 ↾ ∪ 𝐽 ) )
20 sstr2 ⊢ ( 𝑥 ⊆ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) → ( ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ⊆ 𝒫 ran ( 𝐹 ↾ ∪ 𝐽 ) → 𝑥 ⊆ 𝒫 ran ( 𝐹 ↾ ∪ 𝐽 ) ) )
21 19 20 syl5com ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( 𝑥 ⊆ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) → 𝑥 ⊆ 𝒫 ran ( 𝐹 ↾ ∪ 𝐽 ) ) )
22 sspwuni ⊢ ( 𝑥 ⊆ 𝒫 ran ( 𝐹 ↾ ∪ 𝐽 ) ↔ ∪ 𝑥 ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) )
23 21 22 imbitrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( 𝑥 ⊆ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) → ∪ 𝑥 ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) ) )
24 imauni ⊢ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ ∪ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 )
25 14 simplbda ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) → ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ∈ 𝐽 )
26 25 ralrimiva ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ∀ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ∈ 𝐽 )
27 ssralv ⊢ ( 𝑥 ⊆ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) → ( ∀ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ∈ 𝐽 → ∀ 𝑦 ∈ 𝑥 ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ∈ 𝐽 ) )
28 26 27 mpan9 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ 𝑥 ⊆ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) → ∀ 𝑦 ∈ 𝑥 ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ∈ 𝐽 )
29 iunopn ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝑥 ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ∈ 𝐽 ) → ∪ 𝑦 ∈ 𝑥 ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ∈ 𝐽 )
30 4 28 29 syl2an2r ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ 𝑥 ⊆ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) → ∪ 𝑦 ∈ 𝑥 ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ∈ 𝐽 )
31 24 30 eqeltrid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ 𝑥 ⊆ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) → ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ ∪ 𝑥 ) ∈ 𝐽 )
32 31 ex ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( 𝑥 ⊆ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) → ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ ∪ 𝑥 ) ∈ 𝐽 ) )
33 23 32 jcad ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( 𝑥 ⊆ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) → ( ∪ 𝑥 ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ ∪ 𝑥 ) ∈ 𝐽 ) ) )
34 1 elqtop ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐹 ↾ ∪ 𝐽 ) : dom ( 𝐹 ↾ ∪ 𝐽 ) –onto→ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ dom ( 𝐹 ↾ ∪ 𝐽 ) ⊆ ∪ 𝐽 ) → ( ∪ 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ↔ ( ∪ 𝑥 ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ ∪ 𝑥 ) ∈ 𝐽 ) ) )
35 4 8 12 34 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ∪ 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ↔ ( ∪ 𝑥 ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ ∪ 𝑥 ) ∈ 𝐽 ) ) )
36 33 35 sylibrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( 𝑥 ⊆ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) → ∪ 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) )
37 36 alrimiv ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ∀ 𝑥 ( 𝑥 ⊆ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) → ∪ 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) )
38 inss1 ⊢ ( 𝑥 ∩ 𝑦 ) ⊆ 𝑥
39 1 elqtop ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐹 ↾ ∪ 𝐽 ) : dom ( 𝐹 ↾ ∪ 𝐽 ) –onto→ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ dom ( 𝐹 ↾ ∪ 𝐽 ) ⊆ ∪ 𝐽 ) → ( 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ↔ ( 𝑥 ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑥 ) ∈ 𝐽 ) ) )
40 4 8 12 39 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ↔ ( 𝑥 ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑥 ) ∈ 𝐽 ) ) )
41 40 biimpa ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) → ( 𝑥 ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑥 ) ∈ 𝐽 ) )
42 41 adantrr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∧ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) ) → ( 𝑥 ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑥 ) ∈ 𝐽 ) )
43 42 simpld ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∧ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) ) → 𝑥 ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) )
44 38 43 sstrid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∧ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) )
45 6 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∧ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) ) → Fun ( 𝐹 ↾ ∪ 𝐽 ) )
46 inpreima ⊢ ( Fun ( 𝐹 ↾ ∪ 𝐽 ) → ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ ( 𝑥 ∩ 𝑦 ) ) = ( ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑥 ) ∩ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ) )
47 45 46 syl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∧ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) ) → ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ ( 𝑥 ∩ 𝑦 ) ) = ( ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑥 ) ∩ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ) )
48 4 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∧ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) ) → 𝐽 ∈ Top )
49 42 simprd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∧ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) ) → ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑥 ) ∈ 𝐽 )
50 25 adantrl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∧ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) ) → ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ∈ 𝐽 )
51 inopn ⊢ ( ( 𝐽 ∈ Top ∧ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑥 ) ∈ 𝐽 ∧ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ∈ 𝐽 ) → ( ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑥 ) ∩ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ) ∈ 𝐽 )
52 48 49 50 51 syl3anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∧ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) ) → ( ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑥 ) ∩ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ 𝑦 ) ) ∈ 𝐽 )
53 47 52 eqeltrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∧ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) ) → ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ ( 𝑥 ∩ 𝑦 ) ) ∈ 𝐽 )
54 1 elqtop ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐹 ↾ ∪ 𝐽 ) : dom ( 𝐹 ↾ ∪ 𝐽 ) –onto→ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ dom ( 𝐹 ↾ ∪ 𝐽 ) ⊆ ∪ 𝐽 ) → ( ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ↔ ( ( 𝑥 ∩ 𝑦 ) ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ ( 𝑥 ∩ 𝑦 ) ) ∈ 𝐽 ) ) )
55 4 8 12 54 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ↔ ( ( 𝑥 ∩ 𝑦 ) ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ ( 𝑥 ∩ 𝑦 ) ) ∈ 𝐽 ) ) )
56 55 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∧ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) ) → ( ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ↔ ( ( 𝑥 ∩ 𝑦 ) ⊆ ran ( 𝐹 ↾ ∪ 𝐽 ) ∧ ( ◡ ( 𝐹 ↾ ∪ 𝐽 ) “ ( 𝑥 ∩ 𝑦 ) ) ∈ 𝐽 ) ) )
57 44 53 56 mpbir2and ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) ∧ ( 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∧ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) )
58 57 ralrimivva ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ∀ 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∀ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) )
59 ovex ⊢ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∈ V
60 istopg ⊢ ( ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∈ V → ( ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) → ∪ 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) ∧ ∀ 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∀ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) ) )
61 59 60 ax-mp ⊢ ( ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) → ∪ 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) ∧ ∀ 𝑥 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∀ 𝑦 ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ) )
62 37 58 61 sylanbrc ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( 𝐽 qTop ( 𝐹 ↾ ∪ 𝐽 ) ) ∈ Top )
63 3 62 eqeltrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( 𝐽 qTop 𝐹 ) ∈ Top )