Theorem clublem

Description: If a superset Y of X possesses the property parameterized in x in ps , then Y is a superset of the closure of that property for the set X . (Contributed by RP, 23-Jul-2020)

	Ref	Expression
Hypotheses	clublem.y	⊢ ( 𝜑 → 𝑌 ∈ V )
	clublem.sub	⊢ ( 𝑥 = 𝑌 → ( 𝜓 ↔ 𝜒 ) )
	clublem.sup	⊢ ( 𝜑 → 𝑋 ⊆ 𝑌 )
	clublem.maj	⊢ ( 𝜑 → 𝜒 )
Assertion	clublem	⊢ ( 𝜑 → ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) } ⊆ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		clublem.y	⊢ ( 𝜑 → 𝑌 ∈ V )
2		clublem.sub	⊢ ( 𝑥 = 𝑌 → ( 𝜓 ↔ 𝜒 ) )
3		clublem.sup	⊢ ( 𝜑 → 𝑋 ⊆ 𝑌 )
4		clublem.maj	⊢ ( 𝜑 → 𝜒 )
5	1	a1d	⊢ ( 𝜑 → ( ( 𝑋 ⊆ 𝑌 ∧ 𝜒 ) → 𝑌 ∈ V ) )
6	2	cleq2lem	⊢ ( 𝑥 = 𝑌 → ( ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ↔ ( 𝑋 ⊆ 𝑌 ∧ 𝜒 ) ) )
7	6	elab3g	⊢ ( ( ( 𝑋 ⊆ 𝑌 ∧ 𝜒 ) → 𝑌 ∈ V ) → ( 𝑌 ∈ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) } ↔ ( 𝑋 ⊆ 𝑌 ∧ 𝜒 ) ) )
8	5 7	syl	⊢ ( 𝜑 → ( 𝑌 ∈ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) } ↔ ( 𝑋 ⊆ 𝑌 ∧ 𝜒 ) ) )
9	3 4 8	mpbir2and	⊢ ( 𝜑 → 𝑌 ∈ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) } )
10		intss1	⊢ ( 𝑌 ∈ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) } → ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) } ⊆ 𝑌 )
11	9 10	syl	⊢ ( 𝜑 → ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) } ⊆ 𝑌 )