Theorem wunot

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

	Ref	Expression
Hypotheses	wun0.1	$$⊢\phi \to U\in \mathrm{WUni}$$
	wunop.2	$$⊢\phi \to A\in U$$
	wunop.3	$$⊢\phi \to B\in U$$
	wunot.3	$$⊢\phi \to C\in U$$
Assertion	wunot	$$⊢\phi \to ⟨A,B,C⟩\in U$$

Proof

Step	Hyp	Ref	Expression
1		wun0.1	$$⊢\phi \to U\in \mathrm{WUni}$$
2		wunop.2	$$⊢\phi \to A\in U$$
3		wunop.3	$$⊢\phi \to B\in U$$
4		wunot.3	$$⊢\phi \to C\in U$$
5		df-ot	$$⊢⟨A,B,C⟩=⟨⟨A,B⟩,C⟩$$
6	1 2 3	wunop	$$⊢\phi \to ⟨A,B⟩\in U$$
7	1 6 4	wunop	$$⊢\phi \to ⟨⟨A,B⟩,C⟩\in U$$
8	5 7	eqeltrid	$$⊢\phi \to ⟨A,B,C⟩\in U$$