Metamath Proof Explorer

Theorem ustuqtop0

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 ustuqtop0 ⊢ U ∈ UnifOn ⁡ X → N : X ⟶ 𝒫 𝒫 X

Proof

Step Hyp Ref Expression
1 utopustuq.1 ⊢ N = p ∈ X ⟼ ran ⁡ v ∈ U ⟼ v p
2 ustimasn ⊢ U ∈ UnifOn ⁡ X ∧ v ∈ U ∧ p ∈ X → v p ⊆ X
3 2 3expa ⊢ U ∈ UnifOn ⁡ X ∧ v ∈ U ∧ p ∈ X → v p ⊆ X
4 3 an32s ⊢ U ∈ UnifOn ⁡ X ∧ p ∈ X ∧ v ∈ U → v p ⊆ X
5 vex ⊢ v ∈ V
6 5 imaex ⊢ v p ∈ V
7 6 elpw ⊢ v p ∈ 𝒫 X ↔ v p ⊆ X
8 4 7 sylibr ⊢ U ∈ UnifOn ⁡ X ∧ p ∈ X ∧ v ∈ U → v p ∈ 𝒫 X
9 8 ralrimiva ⊢ U ∈ UnifOn ⁡ X ∧ p ∈ X → ∀ v ∈ U v p ∈ 𝒫 X
10 eqid ⊢ v ∈ U ⟼ v p = v ∈ U ⟼ v p
11 10 rnmptss ⊢ ∀ v ∈ U v p ∈ 𝒫 X → ran ⁡ v ∈ U ⟼ v p ⊆ 𝒫 X
12 9 11 syl ⊢ U ∈ UnifOn ⁡ X ∧ p ∈ X → ran ⁡ v ∈ U ⟼ v p ⊆ 𝒫 X
13 mptexg ⊢ U ∈ UnifOn ⁡ X → v ∈ U ⟼ v p ∈ V
14 rnexg ⊢ v ∈ U ⟼ v p ∈ V → ran ⁡ v ∈ U ⟼ v p ∈ V
15 elpwg ⊢ ran ⁡ v ∈ U ⟼ v p ∈ V → ran ⁡ v ∈ U ⟼ v p ∈ 𝒫 𝒫 X ↔ ran ⁡ v ∈ U ⟼ v p ⊆ 𝒫 X
16 13 14 15 3syl ⊢ U ∈ UnifOn ⁡ X → ran ⁡ v ∈ U ⟼ v p ∈ 𝒫 𝒫 X ↔ ran ⁡ v ∈ U ⟼ v p ⊆ 𝒫 X
17 16 adantr ⊢ U ∈ UnifOn ⁡ X ∧ p ∈ X → ran ⁡ v ∈ U ⟼ v p ∈ 𝒫 𝒫 X ↔ ran ⁡ v ∈ U ⟼ v p ⊆ 𝒫 X
18 12 17 mpbird ⊢ U ∈ UnifOn ⁡ X ∧ p ∈ X → ran ⁡ v ∈ U ⟼ v p ∈ 𝒫 𝒫 X
19 18 1 fmptd ⊢ U ∈ UnifOn ⁡ X → N : X ⟶ 𝒫 𝒫 X