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