This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 )