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

Metamath Proof Explorer

Theorem ustuqtoplem

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

Ref Expression
Hypothesis utopustuq.1 ⊢ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
Assertion ustuqtoplem ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∈ ( 𝑁 ‘ 𝑃 ) ↔ ∃ 𝑤 ∈ 𝑈 𝐴 = ( 𝑤 “ { 𝑃 } ) ) )

Proof

Step Hyp Ref Expression
1 utopustuq.1 ⊢ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
2 simpl ⊢ ( ( 𝑝 = 𝑞 ∧ 𝑣 ∈ 𝑈 ) → 𝑝 = 𝑞 )
3 2 sneqd ⊢ ( ( 𝑝 = 𝑞 ∧ 𝑣 ∈ 𝑈 ) → { 𝑝 } = { 𝑞 } )
4 3 imaeq2d ⊢ ( ( 𝑝 = 𝑞 ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 “ { 𝑝 } ) = ( 𝑣 “ { 𝑞 } ) )
5 4 mpteq2dva ⊢ ( 𝑝 = 𝑞 → ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) = ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) )
6 5 rneqd ⊢ ( 𝑝 = 𝑞 → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) = ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) )
7 6 cbvmptv ⊢ ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ) = ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) )
8 1 7 eqtri ⊢ 𝑁 = ( 𝑞 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) )
9 simpr2 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑞 = 𝑃 ∧ 𝑣 ∈ 𝑈 ) ) → 𝑞 = 𝑃 )
10 9 sneqd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑞 = 𝑃 ∧ 𝑣 ∈ 𝑈 ) ) → { 𝑞 } = { 𝑃 } )
11 10 imaeq2d ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑞 = 𝑃 ∧ 𝑣 ∈ 𝑈 ) ) → ( 𝑣 “ { 𝑞 } ) = ( 𝑣 “ { 𝑃 } ) )
12 11 3anassrs ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑞 = 𝑃 ) ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 “ { 𝑞 } ) = ( 𝑣 “ { 𝑃 } ) )
13 12 mpteq2dva ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑞 = 𝑃 ) → ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) = ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )
14 13 rneqd ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑞 = 𝑃 ) → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑞 } ) ) = ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )
15 simpr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 )
16 mptexg ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V )
17 rnexg ⊢ ( ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V )
18 16 17 syl ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V )
19 18 adantr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ∈ V )
20 8 14 15 19 fvmptd2 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑃 ) = ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )
21 20 eleq2d ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐴 ∈ ( 𝑁 ‘ 𝑃 ) ↔ 𝐴 ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ) )
22 imaeq1 ⊢ ( 𝑣 = 𝑤 → ( 𝑣 “ { 𝑃 } ) = ( 𝑤 “ { 𝑃 } ) )
23 22 cbvmptv ⊢ ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) = ( 𝑤 ∈ 𝑈 ↦ ( 𝑤 “ { 𝑃 } ) )
24 23 elrnmpt ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ↔ ∃ 𝑤 ∈ 𝑈 𝐴 = ( 𝑤 “ { 𝑃 } ) ) )
25 21 24 sylan9bb ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∈ ( 𝑁 ‘ 𝑃 ) ↔ ∃ 𝑤 ∈ 𝑈 𝐴 = ( 𝑤 “ { 𝑃 } ) ) )