Metamath Proof Explorer

Theorem qtopcmplem

Description: Lemma for qtopcmp and qtopconn . (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypotheses qtopcmp.1 ⊢ X = ⋃ J
qtopcmplem.1 ⊢ J ∈ A → J ∈ Top
qtopcmplem.2 ⊢ J ∈ A ∧ F : X ⟶ onto ⋃ J qTop F ∧ F ∈ J Cn J qTop F → J qTop F ∈ A
Assertion qtopcmplem ⊢ J ∈ A ∧ F Fn X → J qTop F ∈ A

Proof

Step Hyp Ref Expression
1 qtopcmp.1 ⊢ X = ⋃ J
2 qtopcmplem.1 ⊢ J ∈ A → J ∈ Top
3 qtopcmplem.2 ⊢ J ∈ A ∧ F : X ⟶ onto ⋃ J qTop F ∧ F ∈ J Cn J qTop F → J qTop F ∈ A
4 simpl ⊢ J ∈ A ∧ F Fn X → J ∈ A
5 dffn4 ⊢ F Fn X ↔ F : X ⟶ onto ran ⁡ F
6 5 bilani ⊢ J ∈ A ∧ F Fn X → F : X ⟶ onto ran ⁡ F
7 1 qtopuni ⊢ J ∈ Top ∧ F : X ⟶ onto ran ⁡ F → ran ⁡ F = ⋃ J qTop F
8 2 7 sylan ⊢ J ∈ A ∧ F : X ⟶ onto ran ⁡ F → ran ⁡ F = ⋃ J qTop F
9 5 8 sylan2b ⊢ J ∈ A ∧ F Fn X → ran ⁡ F = ⋃ J qTop F
10 foeq3 ⊢ ran ⁡ F = ⋃ J qTop F → F : X ⟶ onto ran ⁡ F ↔ F : X ⟶ onto ⋃ J qTop F
11 9 10 syl ⊢ J ∈ A ∧ F Fn X → F : X ⟶ onto ran ⁡ F ↔ F : X ⟶ onto ⋃ J qTop F
12 6 11 mpbid ⊢ J ∈ A ∧ F Fn X → F : X ⟶ onto ⋃ J qTop F
13 1 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X
14 2 13 sylib ⊢ J ∈ A → J ∈ TopOn ⁡ X
15 qtopid ⊢ J ∈ TopOn ⁡ X ∧ F Fn X → F ∈ J Cn J qTop F
16 14 15 sylan ⊢ J ∈ A ∧ F Fn X → F ∈ J Cn J qTop F
17 4 12 16 3 syl3anc ⊢ J ∈ A ∧ F Fn X → J qTop F ∈ A