Metamath Proof Explorer


Theorem wunxp

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

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

Proof

Step Hyp Ref Expression
1 wun0.1
 |-  ( ph -> U e. WUni )
2 wunop.2
 |-  ( ph -> A e. U )
3 wunop.3
 |-  ( ph -> B e. U )
4 1 2 3 wunun
 |-  ( ph -> ( A u. B ) e. U )
5 1 4 wunpw
 |-  ( ph -> ~P ( A u. B ) e. U )
6 1 5 wunpw
 |-  ( ph -> ~P ~P ( A u. B ) e. U )
7 xpsspw
 |-  ( A X. B ) C_ ~P ~P ( A u. B )
8 7 a1i
 |-  ( ph -> ( A X. B ) C_ ~P ~P ( A u. B ) )
9 1 6 8 wunss
 |-  ( ph -> ( A X. B ) e. U )