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 ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝐴𝑉 ) → ( 𝐴 ∈ ( 𝑁𝑃 ) ↔ ∃ 𝑤𝑈 𝐴 = ( 𝑤 “ { 𝑃 } ) ) )