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 ( 𝐴 ∈ 𝑉 → ∃ 𝑢 ∈ WUni 𝐴 ⊆ 𝑢 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) = ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω )
2 eqid ⊢ ∪ ran ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) = ∪ ran ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω )
3 1 2 wunex2 ⊢ ( 𝐴 ∈ 𝑉 → ( ∪ ran ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) ∈ WUni ∧ 𝐴 ⊆ ∪ ran ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) ) )
4 sseq2 ⊢ ( 𝑢 = ∪ ran ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) → ( 𝐴 ⊆ 𝑢 ↔ 𝐴 ⊆ ∪ ran ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) ) )
5 4 rspcev ⊢ ( ( ∪ ran ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) ∈ WUni ∧ 𝐴 ⊆ ∪ ran ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) ) → ∃ 𝑢 ∈ WUni 𝐴 ⊆ 𝑢 )
6 3 5 syl ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑢 ∈ WUni 𝐴 ⊆ 𝑢 )