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

Metamath Proof Explorer

Theorem refssex

Description: Every set in a refinement has a superset in the original cover. (Contributed by Jeff Hankins, 18-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

Ref Expression
Assertion refssex ⊢ A Ref B ∧ S ∈ A → ∃ x ∈ B S ⊆ x

Proof

Step Hyp Ref Expression
1 refrel ⊢ Rel ⁡ Ref
2 1 brrelex1i ⊢ A Ref B → A ∈ V
3 eqid ⊢ ⋃ A = ⋃ A
4 eqid ⊢ ⋃ B = ⋃ B
5 3 4 isref ⊢ A ∈ V → A Ref B ↔ ⋃ B = ⋃ A ∧ ∀ y ∈ A ∃ x ∈ B y ⊆ x
6 5 simplbda ⊢ A ∈ V ∧ A Ref B → ∀ y ∈ A ∃ x ∈ B y ⊆ x
7 2 6 mpancom ⊢ A Ref B → ∀ y ∈ A ∃ x ∈ B y ⊆ x
8 sseq1 ⊢ y = S → y ⊆ x ↔ S ⊆ x
9 8 rexbidv ⊢ y = S → ∃ x ∈ B y ⊆ x ↔ ∃ x ∈ B S ⊆ x
10 9 rspccv ⊢ ∀ y ∈ A ∃ x ∈ B y ⊆ x → S ∈ A → ∃ x ∈ B S ⊆ x
11 7 10 syl ⊢ A Ref B → S ∈ A → ∃ x ∈ B S ⊆ x
12 11 imp ⊢ A Ref B ∧ S ∈ A → ∃ x ∈ B S ⊆ x