Metamath Proof Explorer

Theorem ist1-5lem

Description: Lemma for ist1-5 and similar theorems. If A is a topological property which implies T_0, such as T_1 or T_2, the property can be "decomposed" into T_0 and a non-T_0 version of property A (which is defined as stating that the Kolmogorov quotient of the space has property A ). For example, if A is T_1, then the theorem states that a space is T_1 iff it is T_0 and its Kolmogorov quotient is T_1 (we call this property R_0). (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypotheses ist1-5lem.1 ⊢ J ∈ A → J ∈ Kol2
ist1-5lem.2 ⊢ J ≃ KQ ⁡ J → J ∈ A → KQ ⁡ J ∈ A
ist1-5lem.3 ⊢ KQ ⁡ J ≃ J → KQ ⁡ J ∈ A → J ∈ A
Assertion ist1-5lem ⊢ J ∈ A ↔ J ∈ Kol2 ∧ KQ ⁡ J ∈ A

Proof

Step Hyp Ref Expression
1 ist1-5lem.1 ⊢ J ∈ A → J ∈ Kol2
2 ist1-5lem.2 ⊢ J ≃ KQ ⁡ J → J ∈ A → KQ ⁡ J ∈ A
3 ist1-5lem.3 ⊢ KQ ⁡ J ≃ J → KQ ⁡ J ∈ A → J ∈ A
4 kqhmph ⊢ J ∈ Kol2 ↔ J ≃ KQ ⁡ J
5 1 4 sylib ⊢ J ∈ A → J ≃ KQ ⁡ J
6 5 2 mpcom ⊢ J ∈ A → KQ ⁡ J ∈ A
7 1 6 jca ⊢ J ∈ A → J ∈ Kol2 ∧ KQ ⁡ J ∈ A
8 hmphsym ⊢ J ≃ KQ ⁡ J → KQ ⁡ J ≃ J
9 4 8 sylbi ⊢ J ∈ Kol2 → KQ ⁡ J ≃ J
10 9 3 syl ⊢ J ∈ Kol2 → KQ ⁡ J ∈ A → J ∈ A
11 10 imp ⊢ J ∈ Kol2 ∧ KQ ⁡ J ∈ A → J ∈ A
12 7 11 impbii ⊢ J ∈ A ↔ J ∈ Kol2 ∧ KQ ⁡ J ∈ A