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

Metamath Proof Explorer

Theorem refbas

Description: A refinement covers the same set. (Contributed by Jeff Hankins, 18-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

Ref Expression
Hypotheses refbas.1 ⊢ 𝑋 = ∪ 𝐴
refbas.2 ⊢ 𝑌 = ∪ 𝐵
Assertion refbas ( 𝐴 Ref 𝐵 → 𝑌 = 𝑋 )

Proof

Step Hyp Ref Expression
1 refbas.1 ⊢ 𝑋 = ∪ 𝐴
2 refbas.2 ⊢ 𝑌 = ∪ 𝐵
3 refrel ⊢ Rel Ref
4 3 brrelex1i ⊢ ( 𝐴 Ref 𝐵 → 𝐴 ∈ V )
5 1 2 isref ⊢ ( 𝐴 ∈ V → ( 𝐴 Ref 𝐵 ↔ ( 𝑌 = 𝑋 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) )
6 5 simprbda ⊢ ( ( 𝐴 ∈ V ∧ 𝐴 Ref 𝐵 ) → 𝑌 = 𝑋 )
7 4 6 mpancom ⊢ ( 𝐴 Ref 𝐵 → 𝑌 = 𝑋 )