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