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

Metamath Proof Explorer

Theorem ustuqtop5

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

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

Proof

Step Hyp Ref Expression
1 utopustuq.1 ⊢ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
2 ustbasel ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) ∈ 𝑈 )
3 snssi ⊢ ( 𝑝 ∈ 𝑋 → { 𝑝 } ⊆ 𝑋 )
4 dfss ⊢ ( { 𝑝 } ⊆ 𝑋 ↔ { 𝑝 } = ( { 𝑝 } ∩ 𝑋 ) )
5 3 4 sylib ⊢ ( 𝑝 ∈ 𝑋 → { 𝑝 } = ( { 𝑝 } ∩ 𝑋 ) )
6 incom ⊢ ( { 𝑝 } ∩ 𝑋 ) = ( 𝑋 ∩ { 𝑝 } )
7 5 6 eqtr2di ⊢ ( 𝑝 ∈ 𝑋 → ( 𝑋 ∩ { 𝑝 } ) = { 𝑝 } )
8 snnzg ⊢ ( 𝑝 ∈ 𝑋 → { 𝑝 } ≠ ∅ )
9 7 8 eqnetrd ⊢ ( 𝑝 ∈ 𝑋 → ( 𝑋 ∩ { 𝑝 } ) ≠ ∅ )
10 9 adantl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝑋 ∩ { 𝑝 } ) ≠ ∅ )
11 xpima2 ⊢ ( ( 𝑋 ∩ { 𝑝 } ) ≠ ∅ → ( ( 𝑋 × 𝑋 ) “ { 𝑝 } ) = 𝑋 )
12 10 11 syl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( ( 𝑋 × 𝑋 ) “ { 𝑝 } ) = 𝑋 )
13 12 eqcomd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → 𝑋 = ( ( 𝑋 × 𝑋 ) “ { 𝑝 } ) )
14 imaeq1 ⊢ ( 𝑤 = ( 𝑋 × 𝑋 ) → ( 𝑤 “ { 𝑝 } ) = ( ( 𝑋 × 𝑋 ) “ { 𝑝 } ) )
15 14 rspceeqv ⊢ ( ( ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ 𝑋 = ( ( 𝑋 × 𝑋 ) “ { 𝑝 } ) ) → ∃ 𝑤 ∈ 𝑈 𝑋 = ( 𝑤 “ { 𝑝 } ) )
16 2 13 15 syl2an2r ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ∃ 𝑤 ∈ 𝑈 𝑋 = ( 𝑤 “ { 𝑝 } ) )
17 elfvex ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 ∈ V )
18 1 ustuqtoplem ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑋 ∈ V ) → ( 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑤 ∈ 𝑈 𝑋 = ( 𝑤 “ { 𝑝 } ) ) )
19 17 18 mpidan ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑤 ∈ 𝑈 𝑋 = ( 𝑤 “ { 𝑝 } ) ) )
20 16 19 mpbird ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) )