Theorem fincmp

Description: A finite topology is compact. (Contributed by FL, 22-Dec-2008)

	Ref	Expression
Assertion	fincmp	⊢ ( 𝐽 ∈ ( Top ∩ Fin ) → 𝐽 ∈ Comp )

Proof

Step	Hyp	Ref	Expression
1		elinel1	⊢ ( 𝐽 ∈ ( Top ∩ Fin ) → 𝐽 ∈ Top )
2		elinel2	⊢ ( 𝐽 ∈ ( Top ∩ Fin ) → 𝐽 ∈ Fin )
3		vex	⊢ 𝑦 ∈ V
4	3	pwid	⊢ 𝑦 ∈ 𝒫 𝑦
5		velpw	⊢ ( 𝑦 ∈ 𝒫 𝐽 ↔ 𝑦 ⊆ 𝐽 )
6		ssfi	⊢ ( ( 𝐽 ∈ Fin ∧ 𝑦 ⊆ 𝐽 ) → 𝑦 ∈ Fin )
7	5 6	sylan2b	⊢ ( ( 𝐽 ∈ Fin ∧ 𝑦 ∈ 𝒫 𝐽 ) → 𝑦 ∈ Fin )
8		elin	⊢ ( 𝑦 ∈ ( 𝒫 𝑦 ∩ Fin ) ↔ ( 𝑦 ∈ 𝒫 𝑦 ∧ 𝑦 ∈ Fin ) )
9		unieq	⊢ ( 𝑧 = 𝑦 → ∪ 𝑧 = ∪ 𝑦 )
10	9	rspceeqv	⊢ ( ( 𝑦 ∈ ( 𝒫 𝑦 ∩ Fin ) ∧ ∪ 𝐽 = ∪ 𝑦 ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 )
11	10	ex	⊢ ( 𝑦 ∈ ( 𝒫 𝑦 ∩ Fin ) → ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) )
12	8 11	sylbir	⊢ ( ( 𝑦 ∈ 𝒫 𝑦 ∧ 𝑦 ∈ Fin ) → ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) )
13	4 7 12	sylancr	⊢ ( ( 𝐽 ∈ Fin ∧ 𝑦 ∈ 𝒫 𝐽 ) → ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) )
14	13	ralrimiva	⊢ ( 𝐽 ∈ Fin → ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) )
15	2 14	syl	⊢ ( 𝐽 ∈ ( Top ∩ Fin ) → ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) )
16		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
17	16	iscmp	⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) ) )
18	1 15 17	sylanbrc	⊢ ( 𝐽 ∈ ( Top ∩ Fin ) → 𝐽 ∈ Comp )