This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 dfss2 ⊢ ( 𝐴 ⊆ ∪ 𝐽 ↔ ( 𝐴 ∩ ∪ 𝐽 ) = 𝐴 )
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 𝐴 ) )