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 ⊢ φ → J ∈ V
restsubel.2 ⊢ φ → ⋃ J ∈ J
restsubel.3 ⊢ φ → A ⊆ ⋃ J
Assertion restsubel ⊢ φ → A ∈ J ↾ 𝑡 A

Proof

Step Hyp Ref Expression
1 restsubel.1 ⊢ φ → J ∈ V
2 restsubel.2 ⊢ φ → ⋃ J ∈ J
3 restsubel.3 ⊢ φ → A ⊆ ⋃ J
4 ineq1 ⊢ x = ⋃ J → x ∩ A = ⋃ J ∩ A
5 4 eqeq2d ⊢ x = ⋃ J → A = x ∩ A ↔ A = ⋃ J ∩ A
6 5 adantl ⊢ φ ∧ x = ⋃ J → A = x ∩ A ↔ A = ⋃ J ∩ A
7 incom ⊢ ⋃ J ∩ A = A ∩ ⋃ J
8 7 a1i ⊢ φ → ⋃ J ∩ A = A ∩ ⋃ J
9 dfss2 ⊢ A ⊆ ⋃ J ↔ A ∩ ⋃ J = A
10 3 9 sylib ⊢ φ → A ∩ ⋃ J = A
11 8 10 eqtrd ⊢ φ → ⋃ J ∩ A = A
12 11 eqcomd ⊢ φ → A = ⋃ J ∩ A
13 2 6 12 rspcedvd ⊢ φ → ∃ x ∈ J A = x ∩ A
14 2 3 ssexd ⊢ φ → A ∈ V
15 elrest ⊢ J ∈ V ∧ A ∈ V → A ∈ J ↾ 𝑡 A ↔ ∃ x ∈ J A = x ∩ A
16 1 14 15 syl2anc ⊢ φ → A ∈ J ↾ 𝑡 A ↔ ∃ x ∈ J A = x ∩ A
17 13 16 mpbird ⊢ φ → A ∈ J ↾ 𝑡 A