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