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 ⊢ ( 𝜑 → 𝑈 ∈ WUni )
wunress.2 ⊢ ( 𝜑 → ω ∈ 𝑈 )
wunress.3 ⊢ ( 𝜑 → 𝑊 ∈ 𝑈 )
Assertion wunress ( 𝜑 → ( 𝑊 ↾s 𝐴 ) ∈ 𝑈 )

Proof

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