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