Theorem restsubel

Description: A subset belongs in the space it generates via restriction. (Contributed by Glauco Siliprandi, 21-Dec-2024)

	Ref	Expression
Hypotheses	restsubel.1	⊢ ( 𝜑 → 𝐽 ∈ 𝑉 )
	restsubel.2	⊢ ( 𝜑 → ∪ 𝐽 ∈ 𝐽 )
	restsubel.3	⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝐽 )
Assertion	restsubel	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐽 ↾t 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		restsubel.1	⊢ ( 𝜑 → 𝐽 ∈ 𝑉 )
2		restsubel.2	⊢ ( 𝜑 → ∪ 𝐽 ∈ 𝐽 )
3		restsubel.3	⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝐽 )
4		ineq1	⊢ ( 𝑥 = ∪ 𝐽 → ( 𝑥 ∩ 𝐴 ) = ( ∪ 𝐽 ∩ 𝐴 ) )
5	4	eqeq2d	⊢ ( 𝑥 = ∪ 𝐽 → ( 𝐴 = ( 𝑥 ∩ 𝐴 ) ↔ 𝐴 = ( ∪ 𝐽 ∩ 𝐴 ) ) )
6	5	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = ∪ 𝐽 ) → ( 𝐴 = ( 𝑥 ∩ 𝐴 ) ↔ 𝐴 = ( ∪ 𝐽 ∩ 𝐴 ) ) )
7		incom	⊢ ( ∪ 𝐽 ∩ 𝐴 ) = ( 𝐴 ∩ ∪ 𝐽 )
8	7	a1i	⊢ ( 𝜑 → ( ∪ 𝐽 ∩ 𝐴 ) = ( 𝐴 ∩ ∪ 𝐽 ) )
9		df-ss	⊢ ( 𝐴 ⊆ ∪ 𝐽 ↔ ( 𝐴 ∩ ∪ 𝐽 ) = 𝐴 )
10	3 9	sylib	⊢ ( 𝜑 → ( 𝐴 ∩ ∪ 𝐽 ) = 𝐴 )
11	8 10	eqtrd	⊢ ( 𝜑 → ( ∪ 𝐽 ∩ 𝐴 ) = 𝐴 )
12	11	eqcomd	⊢ ( 𝜑 → 𝐴 = ( ∪ 𝐽 ∩ 𝐴 ) )
13	2 6 12	rspcedvd	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐽 𝐴 = ( 𝑥 ∩ 𝐴 ) )
14	2 3	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
15		elrest	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ V ) → ( 𝐴 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐽 𝐴 = ( 𝑥 ∩ 𝐴 ) ) )
16	1 14 15	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐽 𝐴 = ( 𝑥 ∩ 𝐴 ) ) )
17	13 16	mpbird	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐽 ↾t 𝐴 ) )