Theorem ustuqtop3 23501

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

Hypothesis

Ref	Expression
utopustuq.1	⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))

Assertion

Ref	Expression
ustuqtop3	⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)

Distinct variable groups:   𝑣,𝑝,𝑈   𝑋,𝑝,𝑣,𝑎   𝑁,𝑎,𝑝   𝑣,𝑎,𝑈   𝑋,𝑎

Allowed substitution hint:   𝑁(𝑣)

Proof of Theorem ustuqtop3

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fnresi 6618	. . . . . . 7 ⊢ ( I ↾ 𝑋) Fn 𝑋
2		fnsnfv 6908	. . . . . . 7 ⊢ ((( I ↾ 𝑋) Fn 𝑋 ∧ 𝑝 ∈ 𝑋) → {(( I ↾ 𝑋)‘𝑝)} = (( I ↾ 𝑋) “ {𝑝}))
3	1, 2	mpan 688	. . . . . 6 ⊢ (𝑝 ∈ 𝑋 → {(( I ↾ 𝑋)‘𝑝)} = (( I ↾ 𝑋) “ {𝑝}))
4	3	ad4antlr 731	. . . . 5 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → {(( I ↾ 𝑋)‘𝑝)} = (( I ↾ 𝑋) “ {𝑝}))
5		ustdiag 23466	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈) → ( I ↾ 𝑋) ⊆ 𝑤)
6	5	ad5ant14 756	. . . . . 6 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ( I ↾ 𝑋) ⊆ 𝑤)
7		imass1 6044	. . . . . 6 ⊢ (( I ↾ 𝑋) ⊆ 𝑤 → (( I ↾ 𝑋) “ {𝑝}) ⊆ (𝑤 “ {𝑝}))
8	6, 7	syl 17	. . . . 5 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (( I ↾ 𝑋) “ {𝑝}) ⊆ (𝑤 “ {𝑝}))
9	4, 8	eqsstrd 3974	. . . 4 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → {(( I ↾ 𝑋)‘𝑝)} ⊆ (𝑤 “ {𝑝}))
10		fvex 6843	. . . . 5 ⊢ (( I ↾ 𝑋)‘𝑝) ∈ V
11	10	snss 4738	. . . 4 ⊢ ((( I ↾ 𝑋)‘𝑝) ∈ (𝑤 “ {𝑝}) ↔ {(( I ↾ 𝑋)‘𝑝)} ⊆ (𝑤 “ {𝑝}))
12	9, 11	sylibr 233	. . 3 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (( I ↾ 𝑋)‘𝑝) ∈ (𝑤 “ {𝑝}))
13		fvresi 7106	. . . . 5 ⊢ (𝑝 ∈ 𝑋 → (( I ↾ 𝑋)‘𝑝) = 𝑝)
14	13	eqcomd 2743	. . . 4 ⊢ (𝑝 ∈ 𝑋 → 𝑝 = (( I ↾ 𝑋)‘𝑝))
15	14	ad4antlr 731	. . 3 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑝 = (( I ↾ 𝑋)‘𝑝))
16		simpr 486	. . 3 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑎 = (𝑤 “ {𝑝}))
17	12, 15, 16	3eltr4d 2853	. 2 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑝 ∈ 𝑎)
18		utopustuq.1	. . . . 5 ⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))
19	18	ustuqtoplem 23497	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ V) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})))
20	19	elvd 3449	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})))
21	20	biimpa 478	. 2 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝}))
22	17, 21	r19.29a 3156	1 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1541   ∈ wcel 2106  ∃wrex 3071  Vcvv 3442   ⊆ wss 3902  {csn 4578   ↦ cmpt 5180   I cid 5522  ran crn 5626   ↾ cres 5627   “ cima 5628   Fn wfn 6479  ‘cfv 6484  UnifOncust 23457

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5234  ax-sep 5248  ax-nul 5255  ax-pow 5313  ax-pr 5377  ax-un 7655

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3732  df-csb 3848  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4858  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5181  df-id 5523  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6436  df-fun 6486  df-fn 6487  df-f 6488  df-f1 6489  df-fo 6490  df-f1o 6491  df-fv 6492  df-ust 23458

This theorem is referenced by:  ustuqtop  23504  utopsnneiplem  23505