# 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 e. A -> J e. Kol2 )`
ist1-5lem.2
`|- ( J ~= ( KQ ` J ) -> ( J e. A -> ( KQ ` J ) e. A ) )`
ist1-5lem.3
`|- ( ( KQ ` J ) ~= J -> ( ( KQ ` J ) e. A -> J e. A ) )`
Assertion ist1-5lem
`|- ( J e. A <-> ( J e. Kol2 /\ ( KQ ` J ) e. A ) )`

### Proof

Step Hyp Ref Expression
1 ist1-5lem.1
` |-  ( J e. A -> J e. Kol2 )`
2 ist1-5lem.2
` |-  ( J ~= ( KQ ` J ) -> ( J e. A -> ( KQ ` J ) e. A ) )`
3 ist1-5lem.3
` |-  ( ( KQ ` J ) ~= J -> ( ( KQ ` J ) e. A -> J e. A ) )`
4 kqhmph
` |-  ( J e. Kol2 <-> J ~= ( KQ ` J ) )`
5 1 4 sylib
` |-  ( J e. A -> J ~= ( KQ ` J ) )`
6 5 2 mpcom
` |-  ( J e. A -> ( KQ ` J ) e. A )`
7 1 6 jca
` |-  ( J e. A -> ( J e. Kol2 /\ ( KQ ` J ) e. A ) )`
8 hmphsym
` |-  ( J ~= ( KQ ` J ) -> ( KQ ` J ) ~= J )`
9 4 8 sylbi
` |-  ( J e. Kol2 -> ( KQ ` J ) ~= J )`
10 9 3 syl
` |-  ( J e. Kol2 -> ( ( KQ ` J ) e. A -> J e. A ) )`
11 10 imp
` |-  ( ( J e. Kol2 /\ ( KQ ` J ) e. A ) -> J e. A )`
12 7 11 impbii
` |-  ( J e. A <-> ( J e. Kol2 /\ ( KQ ` J ) e. A ) )`