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 ) )