Description: Lemma for ist15 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 nonT_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, 25Aug2015)
Ref  Expression  

Hypotheses  ist15lem.1   ( J e. A > J e. Kol2 ) 

ist15lem.2   ( J ~= ( KQ ` J ) > ( J e. A > ( KQ ` J ) e. A ) ) 

ist15lem.3   ( ( KQ ` J ) ~= J > ( ( KQ ` J ) e. A > J e. A ) ) 

Assertion  ist15lem   ( J e. A <> ( J e. Kol2 /\ ( KQ ` J ) e. A ) ) 
Step  Hyp  Ref  Expression 

1  ist15lem.1   ( J e. A > J e. Kol2 ) 

2  ist15lem.2   ( J ~= ( KQ ` J ) > ( J e. A > ( KQ ` J ) e. A ) ) 

3  ist15lem.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 ) ) 