Theorem wunot

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

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

Proof

Step	Hyp	Ref	Expression
1		wun0.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
2		wunop.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
3		wunop.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
4		wunot.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
5		df-ot	⊢ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩
6	1 2 3	wunop	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑈 )
7	1 6 4	wunop	⊢ ( 𝜑 → ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ ∈ 𝑈 )
8	5 7	eqeltrid	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ∈ 𝑈 )