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 ‘ 𝑋 ) → 𝑁 : 𝑋 ⟶ 𝒫 𝒫 𝑋 )