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 𝐴 ) )