Theorem wunop

Description: A weak universe is closed under ordered pairs. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	wun0.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	wunop.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	wunop.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
Assertion	wunop	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		wun0.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
2		wunop.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
3		wunop.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
4		dfopg	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )
5	2 3 4	syl2anc	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )
6	1 2	wunsn	⊢ ( 𝜑 → { 𝐴 } ∈ 𝑈 )
7	1 2 3	wunpr	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ 𝑈 )
8	1 6 7	wunpr	⊢ ( 𝜑 → { { 𝐴 } , { 𝐴 , 𝐵 } } ∈ 𝑈 )
9	5 8	eqeltrd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑈 )