This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ustuqtop0

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

Ref Expression
Hypothesis utopustuq.1 ⊢ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
Assertion ustuqtop0 ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑁 : 𝑋 ⟶ 𝒫 𝒫 𝑋 )

Proof

Step Hyp Ref Expression
1 utopustuq.1 ⊢ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
2 ustimasn ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ∧ 𝑝 ∈ 𝑋 ) → ( 𝑣 “ { 𝑝 } ) ⊆ 𝑋 )
3 2 3expa ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝑣 “ { 𝑝 } ) ⊆ 𝑋 )
4 3 an32s ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 “ { 𝑝 } ) ⊆ 𝑋 )
5 vex ⊢ 𝑣 ∈ V
6 5 imaex ⊢ ( 𝑣 “ { 𝑝 } ) ∈ V
7 6 elpw ⊢ ( ( 𝑣 “ { 𝑝 } ) ∈ 𝒫 𝑋 ↔ ( 𝑣 “ { 𝑝 } ) ⊆ 𝑋 )
8 4 7 sylibr ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 “ { 𝑝 } ) ∈ 𝒫 𝑋 )
9 8 ralrimiva ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ∀ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ∈ 𝒫 𝑋 )
10 eqid ⊢ ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) = ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) )
11 10 rnmptss ⊢ ( ∀ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑝 } ) ∈ 𝒫 𝑋 → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ⊆ 𝒫 𝑋 )
12 9 11 syl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ⊆ 𝒫 𝑋 )
13 mptexg ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ V )
14 rnexg ⊢ ( ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ V → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ V )
15 elpwg ⊢ ( ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ V → ( ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ 𝒫 𝒫 𝑋 ↔ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ⊆ 𝒫 𝑋 ) )
16 13 14 15 3syl ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ 𝒫 𝒫 𝑋 ↔ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ⊆ 𝒫 𝑋 ) )
17 16 adantr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ 𝒫 𝒫 𝑋 ↔ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ⊆ 𝒫 𝑋 ) )
18 12 17 mpbird ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ∈ 𝒫 𝒫 𝑋 )
19 18 1 fmptd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑁 : 𝑋 ⟶ 𝒫 𝒫 𝑋 )