Theorem wunco

Description: A weak universe is closed under composition. (Contributed by Mario Carneiro, 12-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		wun0.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
2		wunop.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
3		wunco.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
4	1 3	wundm	⊢ ( 𝜑 → dom 𝐵 ∈ 𝑈 )
5		dmcoss	⊢ dom ( 𝐴 ∘ 𝐵 ) ⊆ dom 𝐵
6	5	a1i	⊢ ( 𝜑 → dom ( 𝐴 ∘ 𝐵 ) ⊆ dom 𝐵 )
7	1 4 6	wunss	⊢ ( 𝜑 → dom ( 𝐴 ∘ 𝐵 ) ∈ 𝑈 )
8	1 2	wunrn	⊢ ( 𝜑 → ran 𝐴 ∈ 𝑈 )
9		rncoss	⊢ ran ( 𝐴 ∘ 𝐵 ) ⊆ ran 𝐴
10	9	a1i	⊢ ( 𝜑 → ran ( 𝐴 ∘ 𝐵 ) ⊆ ran 𝐴 )
11	1 8 10	wunss	⊢ ( 𝜑 → ran ( 𝐴 ∘ 𝐵 ) ∈ 𝑈 )
12	1 7 11	wunxp	⊢ ( 𝜑 → ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) ∈ 𝑈 )
13		relco	⊢ Rel ( 𝐴 ∘ 𝐵 )
14		relssdmrn	⊢ ( Rel ( 𝐴 ∘ 𝐵 ) → ( 𝐴 ∘ 𝐵 ) ⊆ ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) )
15	13 14	mp1i	⊢ ( 𝜑 → ( 𝐴 ∘ 𝐵 ) ⊆ ( dom ( 𝐴 ∘ 𝐵 ) × ran ( 𝐴 ∘ 𝐵 ) ) )
16	1 12 15	wunss	⊢ ( 𝜑 → ( 𝐴 ∘ 𝐵 ) ∈ 𝑈 )