Theorem crefi

Description: The property that every open cover has an A refinement for the topological space J . (Contributed by Thierry Arnoux, 7-Jan-2020)

	Ref	Expression
Hypothesis	crefi.x	⊢ 𝑋 = ∪ 𝐽
Assertion	crefi	⊢ ( ( 𝐽 ∈ CovHasRef 𝐴 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶 ) → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) 𝑧 Ref 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		crefi.x	⊢ 𝑋 = ∪ 𝐽
2		simp1	⊢ ( ( 𝐽 ∈ CovHasRef 𝐴 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶 ) → 𝐽 ∈ CovHasRef 𝐴 )
3		simp2	⊢ ( ( 𝐽 ∈ CovHasRef 𝐴 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶 ) → 𝐶 ⊆ 𝐽 )
4	2 3	sselpwd	⊢ ( ( 𝐽 ∈ CovHasRef 𝐴 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶 ) → 𝐶 ∈ 𝒫 𝐽 )
5	1	iscref	⊢ ( 𝐽 ∈ CovHasRef 𝐴 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) ) )
6	5	simprbi	⊢ ( 𝐽 ∈ CovHasRef 𝐴 → ∀ 𝑦 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) )
7	6	3ad2ant1	⊢ ( ( 𝐽 ∈ CovHasRef 𝐴 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶 ) → ∀ 𝑦 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) )
8		simp3	⊢ ( ( 𝐽 ∈ CovHasRef 𝐴 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶 ) → 𝑋 = ∪ 𝐶 )
9		unieq	⊢ ( 𝑦 = 𝐶 → ∪ 𝑦 = ∪ 𝐶 )
10	9	eqeq2d	⊢ ( 𝑦 = 𝐶 → ( 𝑋 = ∪ 𝑦 ↔ 𝑋 = ∪ 𝐶 ) )
11		breq2	⊢ ( 𝑦 = 𝐶 → ( 𝑧 Ref 𝑦 ↔ 𝑧 Ref 𝐶 ) )
12	11	rexbidv	⊢ ( 𝑦 = 𝐶 → ( ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) 𝑧 Ref 𝑦 ↔ ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) 𝑧 Ref 𝐶 ) )
13	10 12	imbi12d	⊢ ( 𝑦 = 𝐶 → ( ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) ↔ ( 𝑋 = ∪ 𝐶 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) 𝑧 Ref 𝐶 ) ) )
14	13	rspcv	⊢ ( 𝐶 ∈ 𝒫 𝐽 → ( ∀ 𝑦 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) → ( 𝑋 = ∪ 𝐶 → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) 𝑧 Ref 𝐶 ) ) )
15	4 7 8 14	syl3c	⊢ ( ( 𝐽 ∈ CovHasRef 𝐴 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶 ) → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ 𝐴 ) 𝑧 Ref 𝐶 )