Description: The closure of a subclass is a subclass of the closure. (Contributed by RP, 16-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | clsslem | ⊢ ( 𝑅 ⊆ 𝑆 → ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ 𝜑 ) } ⊆ ∩ { 𝑟 ∣ ( 𝑆 ⊆ 𝑟 ∧ 𝜑 ) } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstr2 | ⊢ ( 𝑅 ⊆ 𝑆 → ( 𝑆 ⊆ 𝑟 → 𝑅 ⊆ 𝑟 ) ) | |
2 | 1 | anim1d | ⊢ ( 𝑅 ⊆ 𝑆 → ( ( 𝑆 ⊆ 𝑟 ∧ 𝜑 ) → ( 𝑅 ⊆ 𝑟 ∧ 𝜑 ) ) ) |
3 | 2 | ss2abdv | ⊢ ( 𝑅 ⊆ 𝑆 → { 𝑟 ∣ ( 𝑆 ⊆ 𝑟 ∧ 𝜑 ) } ⊆ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ 𝜑 ) } ) |
4 | intss | ⊢ ( { 𝑟 ∣ ( 𝑆 ⊆ 𝑟 ∧ 𝜑 ) } ⊆ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ 𝜑 ) } → ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ 𝜑 ) } ⊆ ∩ { 𝑟 ∣ ( 𝑆 ⊆ 𝑟 ∧ 𝜑 ) } ) | |
5 | 3 4 | syl | ⊢ ( 𝑅 ⊆ 𝑆 → ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ 𝜑 ) } ⊆ ∩ { 𝑟 ∣ ( 𝑆 ⊆ 𝑟 ∧ 𝜑 ) } ) |