This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wunco

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

Ref Expression
Hypotheses wun0.1 
|- ( ph -> U e. WUni )
wunop.2 
|- ( ph -> A e. U )
wunco.3 
|- ( ph -> B e. U )
Assertion wunco 
|- ( ph -> ( A o. B ) e. U )

Proof

Step Hyp Ref Expression
1 wun0.1 
 |-  ( ph -> U e. WUni )
2 wunop.2 
 |-  ( ph -> A e. U )
3 wunco.3 
 |-  ( ph -> B e. U )
4 1 3 wundm 
 |-  ( ph -> dom B e. U )
5 dmcoss 
 |-  dom ( A o. B ) C_ dom B
6 5 a1i 
 |-  ( ph -> dom ( A o. B ) C_ dom B )
7 1 4 6 wunss 
 |-  ( ph -> dom ( A o. B ) e. U )
8 1 2 wunrn 
 |-  ( ph -> ran A e. U )
9 rncoss 
 |-  ran ( A o. B ) C_ ran A
10 9 a1i 
 |-  ( ph -> ran ( A o. B ) C_ ran A )
11 1 8 10 wunss 
 |-  ( ph -> ran ( A o. B ) e. U )
12 1 7 11 wunxp 
 |-  ( ph -> ( dom ( A o. B ) X. ran ( A o. B ) ) e. U )
13 relco 
 |-  Rel ( A o. B )
14 relssdmrn 
 |-  ( Rel ( A o. B ) -> ( A o. B ) C_ ( dom ( A o. B ) X. ran ( A o. B ) ) )
15 13 14 mp1i 
 |-  ( ph -> ( A o. B ) C_ ( dom ( A o. B ) X. ran ( A o. B ) ) )
16 1 12 15 wunss 
 |-  ( ph -> ( A o. B ) e. U )