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

Metamath Proof Explorer

Theorem ustuqtop3

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

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

Proof

Step Hyp Ref Expression
1 utopustuq.1 ⊢ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
2 fnresi ⊢ ( I ↾ 𝑋 ) Fn 𝑋
3 fnsnfv ⊢ ( ( ( I ↾ 𝑋 ) Fn 𝑋 ∧ 𝑝 ∈ 𝑋 ) → { ( ( I ↾ 𝑋 ) ‘ 𝑝 ) } = ( ( I ↾ 𝑋 ) “ { 𝑝 } ) )
4 2 3 mpan ⊢ ( 𝑝 ∈ 𝑋 → { ( ( I ↾ 𝑋 ) ‘ 𝑝 ) } = ( ( I ↾ 𝑋 ) “ { 𝑝 } ) )
5 4 ad4antlr ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → { ( ( I ↾ 𝑋 ) ‘ 𝑝 ) } = ( ( I ↾ 𝑋 ) “ { 𝑝 } ) )
6 ustdiag ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝑈 ) → ( I ↾ 𝑋 ) ⊆ 𝑤 )
7 6 ad5ant14 ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → ( I ↾ 𝑋 ) ⊆ 𝑤 )
8 imass1 ⊢ ( ( I ↾ 𝑋 ) ⊆ 𝑤 → ( ( I ↾ 𝑋 ) “ { 𝑝 } ) ⊆ ( 𝑤 “ { 𝑝 } ) )
9 7 8 syl ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → ( ( I ↾ 𝑋 ) “ { 𝑝 } ) ⊆ ( 𝑤 “ { 𝑝 } ) )
10 5 9 eqsstrd ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → { ( ( I ↾ 𝑋 ) ‘ 𝑝 ) } ⊆ ( 𝑤 “ { 𝑝 } ) )
11 fvex ⊢ ( ( I ↾ 𝑋 ) ‘ 𝑝 ) ∈ V
12 11 snss ⊢ ( ( ( I ↾ 𝑋 ) ‘ 𝑝 ) ∈ ( 𝑤 “ { 𝑝 } ) ↔ { ( ( I ↾ 𝑋 ) ‘ 𝑝 ) } ⊆ ( 𝑤 “ { 𝑝 } ) )
13 10 12 sylibr ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → ( ( I ↾ 𝑋 ) ‘ 𝑝 ) ∈ ( 𝑤 “ { 𝑝 } ) )
14 fvresi ⊢ ( 𝑝 ∈ 𝑋 → ( ( I ↾ 𝑋 ) ‘ 𝑝 ) = 𝑝 )
15 14 eqcomd ⊢ ( 𝑝 ∈ 𝑋 → 𝑝 = ( ( I ↾ 𝑋 ) ‘ 𝑝 ) )
16 15 ad4antlr ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → 𝑝 = ( ( I ↾ 𝑋 ) ‘ 𝑝 ) )
17 simpr ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → 𝑎 = ( 𝑤 “ { 𝑝 } ) )
18 13 16 17 3eltr4d ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ∧ 𝑤 ∈ 𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → 𝑝 ∈ 𝑎 )
19 1 ustuqtoplem ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ V ) → ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑤 ∈ 𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) ) )
20 19 elvd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∃ 𝑤 ∈ 𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) ) )
21 20 biimpa ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑤 ∈ 𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) )
22 18 21 r19.29a ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ 𝑎 )