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 ( ( 𝐴 Ref 𝐵 ∧ 𝑆 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐵 𝑆 ⊆ 𝑥 )

Proof

Step Hyp Ref Expression
1 refrel ⊢ Rel Ref
2 1 brrelex1i ⊢ ( 𝐴 Ref 𝐵 → 𝐴 ∈ V )
3 eqid ⊢ ∪ 𝐴 = ∪ 𝐴
4 eqid ⊢ ∪ 𝐵 = ∪ 𝐵
5 3 4 isref ⊢ ( 𝐴 ∈ V → ( 𝐴 Ref 𝐵 ↔ ( ∪ 𝐵 = ∪ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 𝑦 ⊆ 𝑥 ) ) )
6 5 simplbda ⊢ ( ( 𝐴 ∈ V ∧ 𝐴 Ref 𝐵 ) → ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 𝑦 ⊆ 𝑥 )
7 2 6 mpancom ⊢ ( 𝐴 Ref 𝐵 → ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 𝑦 ⊆ 𝑥 )
8 sseq1 ⊢ ( 𝑦 = 𝑆 → ( 𝑦 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑥 ) )
9 8 rexbidv ⊢ ( 𝑦 = 𝑆 → ( ∃ 𝑥 ∈ 𝐵 𝑦 ⊆ 𝑥 ↔ ∃ 𝑥 ∈ 𝐵 𝑆 ⊆ 𝑥 ) )
10 9 rspccv ⊢ ( ∀ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 𝑦 ⊆ 𝑥 → ( 𝑆 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐵 𝑆 ⊆ 𝑥 ) )
11 7 10 syl ⊢ ( 𝐴 Ref 𝐵 → ( 𝑆 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐵 𝑆 ⊆ 𝑥 ) )
12 11 imp ⊢ ( ( 𝐴 Ref 𝐵 ∧ 𝑆 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐵 𝑆 ⊆ 𝑥 )