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