Metamath Proof Explorer


Theorem ustuqtoplem

Description: Lemma for ustuqtop . (Contributed by Thierry Arnoux, 11-Jan-2018)

Ref Expression
Hypothesis utopustuq.1 N=pXranvUvp
Assertion ustuqtoplem UUnifOnXPXAVANPwUA=wP

Proof

Step Hyp Ref Expression
1 utopustuq.1 N=pXranvUvp
2 simpl p=qvUp=q
3 2 sneqd p=qvUp=q
4 3 imaeq2d p=qvUvp=vq
5 4 mpteq2dva p=qvUvp=vUvq
6 5 rneqd p=qranvUvp=ranvUvq
7 6 cbvmptv pXranvUvp=qXranvUvq
8 1 7 eqtri N=qXranvUvq
9 simpr2 UUnifOnXPXq=PvUq=P
10 9 sneqd UUnifOnXPXq=PvUq=P
11 10 imaeq2d UUnifOnXPXq=PvUvq=vP
12 11 3anassrs UUnifOnXPXq=PvUvq=vP
13 12 mpteq2dva UUnifOnXPXq=PvUvq=vUvP
14 13 rneqd UUnifOnXPXq=PranvUvq=ranvUvP
15 simpr UUnifOnXPXPX
16 mptexg UUnifOnXvUvPV
17 rnexg vUvPVranvUvPV
18 16 17 syl UUnifOnXranvUvPV
19 18 adantr UUnifOnXPXranvUvPV
20 8 14 15 19 fvmptd2 UUnifOnXPXNP=ranvUvP
21 20 eleq2d UUnifOnXPXANPAranvUvP
22 imaeq1 v=wvP=wP
23 22 cbvmptv vUvP=wUwP
24 23 elrnmpt AVAranvUvPwUA=wP
25 21 24 sylan9bb UUnifOnXPXAVANPwUA=wP