Theorem crefss

Description: The "every open cover has an A refinement" predicate respects inclusion. (Contributed by Thierry Arnoux, 7-Jan-2020)

	Ref	Expression
Assertion	crefss	⊢ ( 𝐴 ⊆ 𝐵 → CovHasRef 𝐴 ⊆ CovHasRef 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sslin	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝒫 𝑗 ∩ 𝐴 ) ⊆ ( 𝒫 𝑗 ∩ 𝐵 ) )
2		ssrexv	⊢ ( ( 𝒫 𝑗 ∩ 𝐴 ) ⊆ ( 𝒫 𝑗 ∩ 𝐵 ) → ( ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐵 ) 𝑧 Ref 𝑦 ) )
3	1 2	syl	⊢ ( 𝐴 ⊆ 𝐵 → ( ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐵 ) 𝑧 Ref 𝑦 ) )
4	3	imim2d	⊢ ( 𝐴 ⊆ 𝐵 → ( ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) → ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐵 ) 𝑧 Ref 𝑦 ) ) )
5	4	ralimdv	⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) → ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐵 ) 𝑧 Ref 𝑦 ) ) )
6	5	anim2d	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑗 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) ) → ( 𝑗 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐵 ) 𝑧 Ref 𝑦 ) ) ) )
7		eqid	⊢ ∪ 𝑗 = ∪ 𝑗
8	7	iscref	⊢ ( 𝑗 ∈ CovHasRef 𝐴 ↔ ( 𝑗 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐴 ) 𝑧 Ref 𝑦 ) ) )
9	7	iscref	⊢ ( 𝑗 ∈ CovHasRef 𝐵 ↔ ( 𝑗 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝑗 ( ∪ 𝑗 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑗 ∩ 𝐵 ) 𝑧 Ref 𝑦 ) ) )
10	6 8 9	3imtr4g	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑗 ∈ CovHasRef 𝐴 → 𝑗 ∈ CovHasRef 𝐵 ) )
11	10	ssrdv	⊢ ( 𝐴 ⊆ 𝐵 → CovHasRef 𝐴 ⊆ CovHasRef 𝐵 )