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 | ⊢ ( 𝐽 ∈ 𝐴 → 𝐽 ∈ Kol2 ) | |
| ist1-5lem.2 | ⊢ ( 𝐽 ≃ ( KQ ‘ 𝐽 ) → ( 𝐽 ∈ 𝐴 → ( KQ ‘ 𝐽 ) ∈ 𝐴 ) ) | ||
| ist1-5lem.3 | ⊢ ( ( KQ ‘ 𝐽 ) ≃ 𝐽 → ( ( KQ ‘ 𝐽 ) ∈ 𝐴 → 𝐽 ∈ 𝐴 ) ) | ||
| Assertion | ist1-5lem | ⊢ ( 𝐽 ∈ 𝐴 ↔ ( 𝐽 ∈ Kol2 ∧ ( KQ ‘ 𝐽 ) ∈ 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ist1-5lem.1 | ⊢ ( 𝐽 ∈ 𝐴 → 𝐽 ∈ Kol2 ) | |
| 2 | ist1-5lem.2 | ⊢ ( 𝐽 ≃ ( KQ ‘ 𝐽 ) → ( 𝐽 ∈ 𝐴 → ( KQ ‘ 𝐽 ) ∈ 𝐴 ) ) | |
| 3 | ist1-5lem.3 | ⊢ ( ( KQ ‘ 𝐽 ) ≃ 𝐽 → ( ( KQ ‘ 𝐽 ) ∈ 𝐴 → 𝐽 ∈ 𝐴 ) ) | |
| 4 | kqhmph | ⊢ ( 𝐽 ∈ Kol2 ↔ 𝐽 ≃ ( KQ ‘ 𝐽 ) ) | |
| 5 | 1 4 | sylib | ⊢ ( 𝐽 ∈ 𝐴 → 𝐽 ≃ ( KQ ‘ 𝐽 ) ) |
| 6 | 5 2 | mpcom | ⊢ ( 𝐽 ∈ 𝐴 → ( KQ ‘ 𝐽 ) ∈ 𝐴 ) |
| 7 | 1 6 | jca | ⊢ ( 𝐽 ∈ 𝐴 → ( 𝐽 ∈ Kol2 ∧ ( KQ ‘ 𝐽 ) ∈ 𝐴 ) ) |
| 8 | hmphsym | ⊢ ( 𝐽 ≃ ( KQ ‘ 𝐽 ) → ( KQ ‘ 𝐽 ) ≃ 𝐽 ) | |
| 9 | 4 8 | sylbi | ⊢ ( 𝐽 ∈ Kol2 → ( KQ ‘ 𝐽 ) ≃ 𝐽 ) |
| 10 | 9 3 | syl | ⊢ ( 𝐽 ∈ Kol2 → ( ( KQ ‘ 𝐽 ) ∈ 𝐴 → 𝐽 ∈ 𝐴 ) ) |
| 11 | 10 | imp | ⊢ ( ( 𝐽 ∈ Kol2 ∧ ( KQ ‘ 𝐽 ) ∈ 𝐴 ) → 𝐽 ∈ 𝐴 ) |
| 12 | 7 11 | impbii | ⊢ ( 𝐽 ∈ 𝐴 ↔ ( 𝐽 ∈ Kol2 ∧ ( KQ ‘ 𝐽 ) ∈ 𝐴 ) ) |