Theorem conncompid

Description: The connected component containing A contains A . (Contributed by Mario Carneiro, 19-Mar-2015)

	Ref	Expression
Hypothesis	conncomp.2	⊢ 𝑆 = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) }
Assertion	conncompid	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		conncomp.2	⊢ 𝑆 = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) }
2		simpr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
3	2	snssd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → { 𝐴 } ⊆ 𝑋 )
4		snex	⊢ { 𝐴 } ∈ V
5	4	elpw	⊢ ( { 𝐴 } ∈ 𝒫 𝑋 ↔ { 𝐴 } ⊆ 𝑋 )
6	3 5	sylibr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → { 𝐴 } ∈ 𝒫 𝑋 )
7		snidg	⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ { 𝐴 } )
8	7	adantl	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ { 𝐴 } )
9		restsn2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t { 𝐴 } ) = 𝒫 { 𝐴 } )
10		pwsn	⊢ 𝒫 { 𝐴 } = { ∅ , { 𝐴 } }
11		indisconn	⊢ { ∅ , { 𝐴 } } ∈ Conn
12	10 11	eqeltri	⊢ 𝒫 { 𝐴 } ∈ Conn
13	9 12	eqeltrdi	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t { 𝐴 } ) ∈ Conn )
14	8 13	jca	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ { 𝐴 } ∧ ( 𝐽 ↾t { 𝐴 } ) ∈ Conn ) )
15		eleq2	⊢ ( 𝑥 = { 𝐴 } → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ { 𝐴 } ) )
16		oveq2	⊢ ( 𝑥 = { 𝐴 } → ( 𝐽 ↾t 𝑥 ) = ( 𝐽 ↾t { 𝐴 } ) )
17	16	eleq1d	⊢ ( 𝑥 = { 𝐴 } → ( ( 𝐽 ↾t 𝑥 ) ∈ Conn ↔ ( 𝐽 ↾t { 𝐴 } ) ∈ Conn ) )
18	15 17	anbi12d	⊢ ( 𝑥 = { 𝐴 } → ( ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) ↔ ( 𝐴 ∈ { 𝐴 } ∧ ( 𝐽 ↾t { 𝐴 } ) ∈ Conn ) ) )
19	15 18	anbi12d	⊢ ( 𝑥 = { 𝐴 } → ( ( 𝐴 ∈ 𝑥 ∧ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) ) ↔ ( 𝐴 ∈ { 𝐴 } ∧ ( 𝐴 ∈ { 𝐴 } ∧ ( 𝐽 ↾t { 𝐴 } ) ∈ Conn ) ) ) )
20	19	rspcev	⊢ ( ( { 𝐴 } ∈ 𝒫 𝑋 ∧ ( 𝐴 ∈ { 𝐴 } ∧ ( 𝐴 ∈ { 𝐴 } ∧ ( 𝐽 ↾t { 𝐴 } ) ∈ Conn ) ) ) → ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝐴 ∈ 𝑥 ∧ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) ) )
21	6 8 14 20	syl12anc	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝐴 ∈ 𝑥 ∧ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) ) )
22		elunirab	⊢ ( 𝐴 ∈ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ↔ ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝐴 ∈ 𝑥 ∧ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) ) )
23	21 22	sylibr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } )
24	23 1	eleqtrrdi	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑆 )