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

Metamath Proof Explorer

Theorem wunex

Description: Construct a weak universe from a given set. See also wunex2 . (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion wunex ⊢ A ∈ V → ∃ u ∈ WUni A ⊆ u

Proof

Step Hyp Ref Expression
1 eqid ⊢ rec ⁡ z ∈ V ⟼ z ∪ ⋃ z ∪ ⋃ x ∈ z 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y A ∪ 1 𝑜 ↾ ω = rec ⁡ z ∈ V ⟼ z ∪ ⋃ z ∪ ⋃ x ∈ z 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y A ∪ 1 𝑜 ↾ ω
2 eqid ⊢ ⋃ ran ⁡ rec ⁡ z ∈ V ⟼ z ∪ ⋃ z ∪ ⋃ x ∈ z 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y A ∪ 1 𝑜 ↾ ω = ⋃ ran ⁡ rec ⁡ z ∈ V ⟼ z ∪ ⋃ z ∪ ⋃ x ∈ z 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y A ∪ 1 𝑜 ↾ ω
3 1 2 wunex2 ⊢ A ∈ V → ⋃ ran ⁡ rec ⁡ z ∈ V ⟼ z ∪ ⋃ z ∪ ⋃ x ∈ z 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y A ∪ 1 𝑜 ↾ ω ∈ WUni ∧ A ⊆ ⋃ ran ⁡ rec ⁡ z ∈ V ⟼ z ∪ ⋃ z ∪ ⋃ x ∈ z 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y A ∪ 1 𝑜 ↾ ω
4 sseq2 ⊢ u = ⋃ ran ⁡ rec ⁡ z ∈ V ⟼ z ∪ ⋃ z ∪ ⋃ x ∈ z 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y A ∪ 1 𝑜 ↾ ω → A ⊆ u ↔ A ⊆ ⋃ ran ⁡ rec ⁡ z ∈ V ⟼ z ∪ ⋃ z ∪ ⋃ x ∈ z 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y A ∪ 1 𝑜 ↾ ω
5 4 rspcev ⊢ ⋃ ran ⁡ rec ⁡ z ∈ V ⟼ z ∪ ⋃ z ∪ ⋃ x ∈ z 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y A ∪ 1 𝑜 ↾ ω ∈ WUni ∧ A ⊆ ⋃ ran ⁡ rec ⁡ z ∈ V ⟼ z ∪ ⋃ z ∪ ⋃ x ∈ z 𝒫 x ⋃ x ∪ ran ⁡ y ∈ z ⟼ x y A ∪ 1 𝑜 ↾ ω → ∃ u ∈ WUni A ⊆ u
6 3 5 syl ⊢ A ∈ V → ∃ u ∈ WUni A ⊆ u