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 ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) )