Theorem dispcmp

Description: Every discrete space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020)

	Ref	Expression
Assertion	dispcmp	⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Paracomp )

Proof

Step	Hyp	Ref	Expression
1		distop	⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Top )
2		simpr	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑢 = { 𝑥 } ) → 𝑢 = { 𝑥 } )
3		snelpwi	⊢ ( 𝑥 ∈ 𝑋 → { 𝑥 } ∈ 𝒫 𝑋 )
4	3	adantr	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑢 = { 𝑥 } ) → { 𝑥 } ∈ 𝒫 𝑋 )
5	2 4	eqeltrd	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑢 = { 𝑥 } ) → 𝑢 ∈ 𝒫 𝑋 )
6	5	rexlimiva	⊢ ( ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } → 𝑢 ∈ 𝒫 𝑋 )
7	6	abssi	⊢ { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } ⊆ 𝒫 𝑋
8		simpl	⊢ ( ( 𝑢 = 𝑣 ∧ 𝑥 = 𝑧 ) → 𝑢 = 𝑣 )
9		simpr	⊢ ( ( 𝑢 = 𝑣 ∧ 𝑥 = 𝑧 ) → 𝑥 = 𝑧 )
10	9	sneqd	⊢ ( ( 𝑢 = 𝑣 ∧ 𝑥 = 𝑧 ) → { 𝑥 } = { 𝑧 } )
11	8 10	eqeq12d	⊢ ( ( 𝑢 = 𝑣 ∧ 𝑥 = 𝑧 ) → ( 𝑢 = { 𝑥 } ↔ 𝑣 = { 𝑧 } ) )
12	11	cbvrexdva	⊢ ( 𝑢 = 𝑣 → ( ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } ↔ ∃ 𝑧 ∈ 𝑋 𝑣 = { 𝑧 } ) )
13	12	cbvabv	⊢ { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } = { 𝑣 ∣ ∃ 𝑧 ∈ 𝑋 𝑣 = { 𝑧 } }
14	13	dissnlocfin	⊢ ( 𝑋 ∈ 𝑉 → { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } ∈ ( LocFin ‘ 𝒫 𝑋 ) )
15		elpwg	⊢ ( { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } ∈ ( LocFin ‘ 𝒫 𝑋 ) → ( { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } ∈ 𝒫 𝒫 𝑋 ↔ { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } ⊆ 𝒫 𝑋 ) )
16	14 15	syl	⊢ ( 𝑋 ∈ 𝑉 → ( { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } ∈ 𝒫 𝒫 𝑋 ↔ { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } ⊆ 𝒫 𝑋 ) )
17	7 16	mpbiri	⊢ ( 𝑋 ∈ 𝑉 → { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } ∈ 𝒫 𝒫 𝑋 )
18	17	ad2antrr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋 ) ∧ 𝑋 = ∪ 𝑦 ) → { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } ∈ 𝒫 𝒫 𝑋 )
19	14	ad2antrr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋 ) ∧ 𝑋 = ∪ 𝑦 ) → { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } ∈ ( LocFin ‘ 𝒫 𝑋 ) )
20	18 19	elind	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋 ) ∧ 𝑋 = ∪ 𝑦 ) → { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } ∈ ( 𝒫 𝒫 𝑋 ∩ ( LocFin ‘ 𝒫 𝑋 ) ) )
21		simpll	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋 ) ∧ 𝑋 = ∪ 𝑦 ) → 𝑋 ∈ 𝑉 )
22		simpr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋 ) ∧ 𝑋 = ∪ 𝑦 ) → 𝑋 = ∪ 𝑦 )
23	22	eqcomd	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋 ) ∧ 𝑋 = ∪ 𝑦 ) → ∪ 𝑦 = 𝑋 )
24	13	dissnref	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∪ 𝑦 = 𝑋 ) → { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } Ref 𝑦 )
25	21 23 24	syl2anc	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋 ) ∧ 𝑋 = ∪ 𝑦 ) → { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } Ref 𝑦 )
26		breq1	⊢ ( 𝑧 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } → ( 𝑧 Ref 𝑦 ↔ { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } Ref 𝑦 ) )
27	26	rspcev	⊢ ( ( { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } ∈ ( 𝒫 𝒫 𝑋 ∩ ( LocFin ‘ 𝒫 𝑋 ) ) ∧ { 𝑢 ∣ ∃ 𝑥 ∈ 𝑋 𝑢 = { 𝑥 } } Ref 𝑦 ) → ∃ 𝑧 ∈ ( 𝒫 𝒫 𝑋 ∩ ( LocFin ‘ 𝒫 𝑋 ) ) 𝑧 Ref 𝑦 )
28	20 25 27	syl2anc	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋 ) ∧ 𝑋 = ∪ 𝑦 ) → ∃ 𝑧 ∈ ( 𝒫 𝒫 𝑋 ∩ ( LocFin ‘ 𝒫 𝑋 ) ) 𝑧 Ref 𝑦 )
29	28	ex	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝒫 𝑋 ) → ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝒫 𝑋 ∩ ( LocFin ‘ 𝒫 𝑋 ) ) 𝑧 Ref 𝑦 ) )
30	29	ralrimiva	⊢ ( 𝑋 ∈ 𝑉 → ∀ 𝑦 ∈ 𝒫 𝒫 𝑋 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝒫 𝑋 ∩ ( LocFin ‘ 𝒫 𝑋 ) ) 𝑧 Ref 𝑦 ) )
31		unipw	⊢ ∪ 𝒫 𝑋 = 𝑋
32	31	eqcomi	⊢ 𝑋 = ∪ 𝒫 𝑋
33	32	iscref	⊢ ( 𝒫 𝑋 ∈ CovHasRef ( LocFin ‘ 𝒫 𝑋 ) ↔ ( 𝒫 𝑋 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝒫 𝑋 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝒫 𝑋 ∩ ( LocFin ‘ 𝒫 𝑋 ) ) 𝑧 Ref 𝑦 ) ) )
34	1 30 33	sylanbrc	⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ CovHasRef ( LocFin ‘ 𝒫 𝑋 ) )
35		ispcmp	⊢ ( 𝒫 𝑋 ∈ Paracomp ↔ 𝒫 𝑋 ∈ CovHasRef ( LocFin ‘ 𝒫 𝑋 ) )
36	34 35	sylibr	⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Paracomp )