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 ⟼ v p
Assertion ustuqtoplem ⊢ U ∈ UnifOn ⁡ X ∧ P ∈ X ∧ A ∈ V → A ∈ N ⁡ P ↔ ∃ w ∈ U A = w P

Proof

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