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 𝐴 ⊆ 𝑢 )