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

Metamath Proof Explorer

Theorem wunress

Description: Closure of structure restriction in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017) (Proof shortened by AV, 28-Oct-2024)

Ref Expression
Hypotheses wunress.1 ⊢ φ → U ∈ WUni
wunress.2 ⊢ φ → ω ∈ U
wunress.3 ⊢ φ → W ∈ U
Assertion wunress ⊢ φ → W ↾ 𝑠 A ∈ U

Proof

Step Hyp Ref Expression
1 wunress.1 ⊢ φ → U ∈ WUni
2 wunress.2 ⊢ φ → ω ∈ U
3 wunress.3 ⊢ φ → W ∈ U
4 eqid ⊢ W ↾ 𝑠 A = W ↾ 𝑠 A
5 eqid ⊢ Base W = Base W
6 4 5 ressval ⊢ W ∈ U ∧ A ∈ V → W ↾ 𝑠 A = if Base W ⊆ A W W sSet Base ndx A ∩ Base W
7 3 6 sylan ⊢ φ ∧ A ∈ V → W ↾ 𝑠 A = if Base W ⊆ A W W sSet Base ndx A ∩ Base W
8 1 2 basndxelwund ⊢ φ → Base ndx ∈ U
9 incom ⊢ A ∩ Base W = Base W ∩ A
10 baseid ⊢ Base = Slot Base ndx
11 10 1 3 wunstr ⊢ φ → Base W ∈ U
12 1 11 wunin ⊢ φ → Base W ∩ A ∈ U
13 9 12 eqeltrid ⊢ φ → A ∩ Base W ∈ U
14 1 8 13 wunop ⊢ φ → Base ndx A ∩ Base W ∈ U
15 1 3 14 wunsets ⊢ φ → W sSet Base ndx A ∩ Base W ∈ U
16 3 15 ifcld ⊢ φ → if Base W ⊆ A W W sSet Base ndx A ∩ Base W ∈ U
17 16 adantr ⊢ φ ∧ A ∈ V → if Base W ⊆ A W W sSet Base ndx A ∩ Base W ∈ U
18 7 17 eqeltrd ⊢ φ ∧ A ∈ V → W ↾ 𝑠 A ∈ U
19 18 ex ⊢ φ → A ∈ V → W ↾ 𝑠 A ∈ U
20 1 wun0 ⊢ φ → ∅ ∈ U
21 reldmress ⊢ Rel ⁡ dom ⁡ ↾ 𝑠
22 21 ovprc2 ⊢ ¬ A ∈ V → W ↾ 𝑠 A = ∅
23 22 eleq1d ⊢ ¬ A ∈ V → W ↾ 𝑠 A ∈ U ↔ ∅ ∈ U
24 20 23 syl5ibrcom ⊢ φ → ¬ A ∈ V → W ↾ 𝑠 A ∈ U
25 19 24 pm2.61d ⊢ φ → W ↾ 𝑠 A ∈ U