Theorem connsubclo

Description: If a clopen set meets a connected subspace, it must contain the entire subspace. (Contributed by Mario Carneiro, 10-Mar-2015)

	Ref	Expression
Hypotheses	connsubclo.1	|- X = U. J
	connsubclo.3	|- ( ph -> A C_ X )
	connsubclo.4	|- ( ph -> ( J |`t A ) e. Conn )
	connsubclo.5	|- ( ph -> B e. J )
	connsubclo.6	|- ( ph -> ( B i^i A ) =/= (/) )
	connsubclo.7	|- ( ph -> B e. ( Clsd ` J ) )
Assertion	connsubclo	|- ( ph -> A C_ B )

Proof

Step	Hyp	Ref	Expression
1		connsubclo.1	|- X = U. J
2		connsubclo.3	|- ( ph -> A C_ X )
3		connsubclo.4	|- ( ph -> ( J |`t A ) e. Conn )
4		connsubclo.5	|- ( ph -> B e. J )
5		connsubclo.6	|- ( ph -> ( B i^i A ) =/= (/) )
6		connsubclo.7	|- ( ph -> B e. ( Clsd ` J ) )
7		eqid	|- U. ( J |`t A ) = U. ( J |`t A )
8		cldrcl	|- ( B e. ( Clsd ` J ) -> J e. Top )
9	6 8	syl	|- ( ph -> J e. Top )
10	1	topopn	|- ( J e. Top -> X e. J )
11	9 10	syl	|- ( ph -> X e. J )
12	11 2	ssexd	|- ( ph -> A e. _V )
13		elrestr	|- ( ( J e. Top /\ A e. _V /\ B e. J ) -> ( B i^i A ) e. ( J |`t A ) )
14	9 12 4 13	syl3anc	|- ( ph -> ( B i^i A ) e. ( J |`t A ) )
15		eqid	|- ( B i^i A ) = ( B i^i A )
16		ineq1	|- ( x = B -> ( x i^i A ) = ( B i^i A ) )
17	16	rspceeqv	|- ( ( B e. ( Clsd ` J ) /\ ( B i^i A ) = ( B i^i A ) ) -> E. x e. ( Clsd ` J ) ( B i^i A ) = ( x i^i A ) )
18	6 15 17	sylancl	|- ( ph -> E. x e. ( Clsd ` J ) ( B i^i A ) = ( x i^i A ) )
19	1	restcld	|- ( ( J e. Top /\ A C_ X ) -> ( ( B i^i A ) e. ( Clsd ` ( J |`t A ) ) <-> E. x e. ( Clsd ` J ) ( B i^i A ) = ( x i^i A ) ) )
20	9 2 19	syl2anc	|- ( ph -> ( ( B i^i A ) e. ( Clsd ` ( J |`t A ) ) <-> E. x e. ( Clsd ` J ) ( B i^i A ) = ( x i^i A ) ) )
21	18 20	mpbird	|- ( ph -> ( B i^i A ) e. ( Clsd ` ( J |`t A ) ) )
22	7 3 14 5 21	connclo	|- ( ph -> ( B i^i A ) = U. ( J |`t A ) )
23	1	restuni	|- ( ( J e. Top /\ A C_ X ) -> A = U. ( J |`t A ) )
24	9 2 23	syl2anc	|- ( ph -> A = U. ( J |`t A ) )
25	22 24	eqtr4d	|- ( ph -> ( B i^i A ) = A )
26		sseqin2	|- ( A C_ B <-> ( B i^i A ) = A )
27	25 26	sylibr	|- ( ph -> A C_ B )