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

Metamath Proof Explorer

Theorem sess1

Description: Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion sess1 ( 𝑅 ⊆ 𝑆 → ( 𝑆 Se 𝐴 → 𝑅 Se 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑅 ⊆ 𝑆 ∧ 𝑦 ∈ 𝐴 ) → 𝑅 ⊆ 𝑆 )
2 1 ssbrd ⊢ ( ( 𝑅 ⊆ 𝑆 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 𝑅 𝑥 → 𝑦 𝑆 𝑥 ) )
3 2 ss2rabdv ⊢ ( 𝑅 ⊆ 𝑆 → { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ⊆ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑆 𝑥 } )
4 ssexg ⊢ ( ( { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ⊆ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑆 𝑥 } ∧ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑆 𝑥 } ∈ V ) → { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )
5 4 ex ⊢ ( { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ⊆ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑆 𝑥 } → ( { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑆 𝑥 } ∈ V → { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V ) )
6 3 5 syl ⊢ ( 𝑅 ⊆ 𝑆 → ( { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑆 𝑥 } ∈ V → { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V ) )
7 6 ralimdv ⊢ ( 𝑅 ⊆ 𝑆 → ( ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑆 𝑥 } ∈ V → ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V ) )
8 df-se ⊢ ( 𝑆 Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑆 𝑥 } ∈ V )
9 df-se ⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )
10 7 8 9 3imtr4g ⊢ ( 𝑅 ⊆ 𝑆 → ( 𝑆 Se 𝐴 → 𝑅 Se 𝐴 ) )