Theorem ssref

Description: A subcover is a refinement of the original cover. (Contributed by Jeff Hankins, 18-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

	Ref	Expression
Hypotheses	ssref.1	⊢ 𝑋 = ∪ 𝐴
	ssref.2	⊢ 𝑌 = ∪ 𝐵
Assertion	ssref	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) → 𝐴 Ref 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ssref.1	⊢ 𝑋 = ∪ 𝐴
2		ssref.2	⊢ 𝑌 = ∪ 𝐵
3		eqcom	⊢ ( 𝑋 = 𝑌 ↔ 𝑌 = 𝑋 )
4	3	biimpi	⊢ ( 𝑋 = 𝑌 → 𝑌 = 𝑋 )
5	4	3ad2ant3	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) → 𝑌 = 𝑋 )
6		ssel2	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
7	6	3ad2antl2	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
8		ssid	⊢ 𝑥 ⊆ 𝑥
9		sseq2	⊢ ( 𝑦 = 𝑥 → ( 𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ 𝑥 ) )
10	9	rspcev	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ⊆ 𝑥 ) → ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 )
11	7 8 10	sylancl	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 )
12	11	ralrimiva	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 )
13	1 2	isref	⊢ ( 𝐴 ∈ 𝐶 → ( 𝐴 Ref 𝐵 ↔ ( 𝑌 = 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) )
14	13	3ad2ant1	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) → ( 𝐴 Ref 𝐵 ↔ ( 𝑌 = 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) )
15	5 12 14	mpbir2and	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌 ) → 𝐴 Ref 𝐵 )