Metamath Proof Explorer

Theorem ustuqtoplem

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

Ref Expression
Hypothesis utopustuq.1 ⊢N=p∈X⟼ran⁡v∈U⟼vp
Assertion ustuqtoplem ⊢U∈UnifOn⁡X∧P∈X∧A∈V→A∈N⁡P↔∃w∈UA=wP

Proof

Step Hyp Ref Expression
1 utopustuq.1 ⊢N=p∈X⟼ran⁡v∈U⟼vp
2 simpl ⊢p=q∧v∈U→p=q
3 2 sneqd ⊢p=q∧v∈U→p=q
4 3 imaeq2d ⊢p=q∧v∈U→vp=vq
5 4 mpteq2dva ⊢p=q→v∈U⟼vp=v∈U⟼vq
6 5 rneqd ⊢p=q→ran⁡v∈U⟼vp=ran⁡v∈U⟼vq
7 6 cbvmptv ⊢p∈X⟼ran⁡v∈U⟼vp=q∈X⟼ran⁡v∈U⟼vq
8 1 7 eqtri ⊢N=q∈X⟼ran⁡v∈U⟼vq
9 simpr2 ⊢U∈UnifOn⁡X∧P∈X∧q=P∧v∈U→q=P
10 9 sneqd ⊢U∈UnifOn⁡X∧P∈X∧q=P∧v∈U→q=P
11 10 imaeq2d ⊢U∈UnifOn⁡X∧P∈X∧q=P∧v∈U→vq=vP
12 11 3anassrs ⊢U∈UnifOn⁡X∧P∈X∧q=P∧v∈U→vq=vP
13 12 mpteq2dva ⊢U∈UnifOn⁡X∧P∈X∧q=P→v∈U⟼vq=v∈U⟼vP
14 13 rneqd ⊢U∈UnifOn⁡X∧P∈X∧q=P→ran⁡v∈U⟼vq=ran⁡v∈U⟼vP
15 simpr ⊢U∈UnifOn⁡X∧P∈X→P∈X
16 mptexg ⊢U∈UnifOn⁡X→v∈U⟼vP∈V
17 rnexg ⊢v∈U⟼vP∈V→ran⁡v∈U⟼vP∈V
18 16 17 syl ⊢U∈UnifOn⁡X→ran⁡v∈U⟼vP∈V
19 18 adantr ⊢U∈UnifOn⁡X∧P∈X→ran⁡v∈U⟼vP∈V
20 8 14 15 19 fvmptd2 ⊢U∈UnifOn⁡X∧P∈X→N⁡P=ran⁡v∈U⟼vP
21 20 eleq2d ⊢U∈UnifOn⁡X∧P∈X→A∈N⁡P↔A∈ran⁡v∈U⟼vP
22 imaeq1 ⊢v=w→vP=wP
23 22 cbvmptv ⊢v∈U⟼vP=w∈U⟼wP
24 23 elrnmpt ⊢A∈V→A∈ran⁡v∈U⟼vP↔∃w∈UA=wP
25 21 24 sylan9bb ⊢U∈UnifOn⁡X∧P∈X∧A∈V→A∈N⁡P↔∃w∈UA=wP