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

Metamath Proof Explorer

Theorem sess2

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

Ref Expression
Assertion sess2 ( 𝐴 ⊆ 𝐵 → ( 𝑅 Se 𝐵 → 𝑅 Se 𝐴 ) )

Proof

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