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