Theorem sshauslem

Description: Lemma for sshaus and similar theorems. If the topological property A is preserved under injective preimages, then a topology finer than one with property A also has property A . (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Hypotheses	t1sep.1	|- X = U. J
	sshauslem.2	|- ( J e. A -> J e. Top )
	sshauslem.3	|- ( ( J e. A /\ ( _I |` X ) : X -1-1-> X /\ ( _I |` X ) e. ( K Cn J ) ) -> K e. A )
Assertion	sshauslem	|- ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> K e. A )

Proof

Step	Hyp	Ref	Expression
1		t1sep.1	|- X = U. J
2		sshauslem.2	|- ( J e. A -> J e. Top )
3		sshauslem.3	|- ( ( J e. A /\ ( _I |` X ) : X -1-1-> X /\ ( _I |` X ) e. ( K Cn J ) ) -> K e. A )
4		simp1	|- ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> J e. A )
5		f1oi	|- ( _I |` X ) : X -1-1-onto-> X
6		f1of1	|- ( ( _I |` X ) : X -1-1-onto-> X -> ( _I |` X ) : X -1-1-> X )
7	5 6	mp1i	|- ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( _I |` X ) : X -1-1-> X )
8		simp3	|- ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> J C_ K )
9		simp2	|- ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> K e. ( TopOn ` X ) )
10	2	3ad2ant1	|- ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> J e. Top )
11	1	toptopon	|- ( J e. Top <-> J e. ( TopOn ` X ) )
12	10 11	sylib	|- ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> J e. ( TopOn ` X ) )
13		ssidcn	|- ( ( K e. ( TopOn ` X ) /\ J e. ( TopOn ` X ) ) -> ( ( _I |` X ) e. ( K Cn J ) <-> J C_ K ) )
14	9 12 13	syl2anc	|- ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( ( _I |` X ) e. ( K Cn J ) <-> J C_ K ) )
15	8 14	mpbird	|- ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> ( _I |` X ) e. ( K Cn J ) )
16	4 7 15 3	syl3anc	|- ( ( J e. A /\ K e. ( TopOn ` X ) /\ J C_ K ) -> K e. A )