Metamath Proof Explorer


Theorem wuntpos

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

Ref Expression
Hypotheses wun0.1 φUWUni
wunop.2 φAU
Assertion wuntpos φtposAU

Proof

Step Hyp Ref Expression
1 wun0.1 φUWUni
2 wunop.2 φAU
3 1 2 wundm φdomAU
4 1 3 wuncnv φdomA-1U
5 1 wun0 φU
6 1 5 wunsn φU
7 1 4 6 wunun φdomA-1U
8 1 2 wunrn φranAU
9 1 7 8 wunxp φdomA-1×ranAU
10 tposssxp tposAdomA-1×ranA
11 10 a1i φtposAdomA-1×ranA
12 1 9 11 wunss φtposAU