Theorem crefeq

Description: Equality theorem for the "every open cover has an A refinement" predicate. (Contributed by Thierry Arnoux, 7-Jan-2020)

	Ref	Expression
Assertion	crefeq	⊢ ( 𝐴 = 𝐵 → CovHasRef 𝐴 = CovHasRef 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ineq2	⊢ ( 𝐴 = 𝐵 → ( 𝒫 𝑗 ∩ 𝐴 ) = ( 𝒫 𝑗 ∩ 𝐵 ) )
2	1	rexeqdv	⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 ↔ ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐵 ) 𝑧 Ref 𝑦 ) )
3	2	imbi2d	⊢ ( 𝐴 = 𝐵 → ( ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) ↔ ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐵 ) 𝑧 Ref 𝑦 ) ) )
4	3	ralbidv	⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) ↔ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐵 ) 𝑧 Ref 𝑦 ) ) )
5	4	rabbidv	⊢ ( 𝐴 = 𝐵 → { 𝑗 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) } = { 𝑗 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐵 ) 𝑧 Ref 𝑦 ) } )
6		df-cref	⊢ CovHasRef 𝐴 = { 𝑗 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) }
7		df-cref	⊢ CovHasRef 𝐵 = { 𝑗 ∈ Top ∣ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐵 ) 𝑧 Ref 𝑦 ) }
8	5 6 7	3eqtr4g	⊢ ( 𝐴 = 𝐵 → CovHasRef 𝐴 = CovHasRef 𝐵 )