ustuqtop4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ustuqtop4		Structured version Visualization version GIF version

Theorem ustuqtop4 22048

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

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

**Assertion**
Ref	Expression
ustuqtop4	⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))

Distinct variable groups: 𝑣,𝑞,𝑝,𝑈 𝑋,𝑝,𝑞,𝑣 𝑎,𝑏,𝑝,𝑞,𝑁 𝑣,𝑎,𝑈,𝑏 𝑋,𝑎,𝑏 Allowed substitution hint: 𝑁(𝑣)

Proof of Theorem ustuqtop4 Dummy variables 𝑤 𝑟 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplll 798	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋))
2		simplr 792	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → 𝑢 ∈ 𝑈)
3		eqid 2622	. . . . . . . . . . 11 ⊢ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})
4		imaeq1 5461	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
5	4	eqeq2d 2632	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑢 → ((𝑢 “ {𝑝}) = (𝑤 “ {𝑝}) ↔ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})))
6	5	rspcev 3309	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ 𝑈 ∧ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
7	3, 6	mpan2 707	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑈 → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
8	7	adantl 482	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
9		imaexg 7103	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑈 → (𝑢 “ {𝑝}) ∈ V)
10		utopustuq.1	. . . . . . . . . . 11 ⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))
11	10	ustuqtoplem 22043	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑢 “ {𝑝}) ∈ V) → ((𝑢 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
12	9, 11	sylan2 491	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ((𝑢 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
13	8, 12	mpbird 247	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → (𝑢 “ {𝑝}) ∈ (𝑁‘𝑝))
14	1, 2, 13	syl2anc 693	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ∈ (𝑁‘𝑝))
15		simp-5l 808	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑈 ∈ (UnifOn‘𝑋))
16	1	simpld 475	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → 𝑈 ∈ (UnifOn‘𝑋))
17		simp-4r 807	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → 𝑝 ∈ 𝑋)
18		ustimasn 22032	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ 𝑝 ∈ 𝑋) → (𝑢 “ {𝑝}) ⊆ 𝑋)
19	16, 2, 17, 18	syl3anc 1326	. . . . . . . . . . . . 13 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ⊆ 𝑋)
20	19	sselda 3603	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑞 ∈ 𝑋)
21	15, 20	jca 554	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋))
22		simplr 792	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞 ∈ (𝑢 “ {𝑝}))
23		simp-6l 810	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑈 ∈ (UnifOn‘𝑋))
24		simp-4r 807	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑢 ∈ 𝑈)
25		ustrel 22015	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → Rel 𝑢)
26	23, 24, 25	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑢)
27		elrelimasn 5489	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel 𝑢 → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
28	26, 27	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
29	22, 28	mpbid 222	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑢𝑞)
30		simpr 477	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑢 “ {𝑞}))
31		elrelimasn 5489	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel 𝑢 → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
32	26, 31	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
33	30, 32	mpbid 222	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞𝑢𝑟)
34		vex 3203	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑝 ∈ V
35		vex 3203	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑟 ∈ V
36	34, 35	brco 5292	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝(𝑢 ∘ 𝑢)𝑟 ↔ ∃𝑞(𝑝𝑢𝑞 ∧ 𝑞𝑢𝑟))
37	36	biimpri 218	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑞(𝑝𝑢𝑞 ∧ 𝑞𝑢𝑟) → 𝑝(𝑢 ∘ 𝑢)𝑟)
38	37	19.23bi 2061	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝𝑢𝑞 ∧ 𝑞𝑢𝑟) → 𝑝(𝑢 ∘ 𝑢)𝑟)
39	29, 33, 38	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝(𝑢 ∘ 𝑢)𝑟)
40		simpllr 799	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑢 ∘ 𝑢) ⊆ 𝑤)
41	40	ssbrd 4696	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑝(𝑢 ∘ 𝑢)𝑟 → 𝑝𝑤𝑟))
42	39, 41	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑤𝑟)
43		simp-5r 809	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑤 ∈ 𝑈)
44		ustrel 22015	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈) → Rel 𝑤)
45	23, 43, 44	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑤)
46		elrelimasn 5489	. . . . . . . . . . . . . . 15 ⊢ (Rel 𝑤 → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
47	45, 46	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
48	42, 47	mpbird 247	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑤 “ {𝑝}))
49	48	ex 450	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑟 ∈ (𝑢 “ {𝑞}) → 𝑟 ∈ (𝑤 “ {𝑝})))
50	49	ssrdv 3609	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}))
51		simp-4r 807	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑤 ∈ 𝑈)
52	17	adantr 481	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑝 ∈ 𝑋)
53		ustimasn 22032	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈 ∧ 𝑝 ∈ 𝑋) → (𝑤 “ {𝑝}) ⊆ 𝑋)
54	15, 51, 52, 53	syl3anc 1326	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ⊆ 𝑋)
55	21, 50, 54	3jca 1242	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋))
56		simpllr 799	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑢 ∈ 𝑈)
57		eqidd 2623	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ 𝑈 → (𝑢 “ {𝑞}) = (𝑢 “ {𝑞}))
58		imaeq1 5461	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑢 → (𝑤 “ {𝑞}) = (𝑢 “ {𝑞}))
59	58	eqeq2d 2632	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑢 → ((𝑢 “ {𝑞}) = (𝑤 “ {𝑞}) ↔ (𝑢 “ {𝑞}) = (𝑢 “ {𝑞})))
60	59	rspcev 3309	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ 𝑈 ∧ (𝑢 “ {𝑞}) = (𝑢 “ {𝑞})) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
61	57, 60	mpdan 702	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑈 → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
62	61	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
63		imaexg 7103	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑈 → (𝑢 “ {𝑞}) ∈ V)
64	10	ustuqtoplem 22043	. . . . . . . . . . . . 13 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ V) → ((𝑢 “ {𝑞}) ∈ (𝑁‘𝑞) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
65	63, 64	sylan2 491	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ((𝑢 “ {𝑞}) ∈ (𝑁‘𝑞) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
66	62, 65	mpbird 247	. . . . . . . . . . 11 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))
67	15, 20, 56, 66	syl21anc 1325	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))
68	55, 67	jca 554	. . . . . . . . 9 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)))
69		imaexg 7103	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑈 → (𝑤 “ {𝑝}) ∈ V)
70		sseq2 3627	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((𝑢 “ {𝑞}) ⊆ 𝑏 ↔ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝})))
71		sseq1 3626	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ⊆ 𝑋 ↔ (𝑤 “ {𝑝}) ⊆ 𝑋))
72	70, 71	3anbi23d 1402	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋)))
73	72	anbi1d 741	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))))
74	73	anbi1d 741	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈)))
75		eleq1 2689	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ∈ (𝑁‘𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
76	74, 75	imbi12d 334	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → 𝑏 ∈ (𝑁‘𝑞)) ↔ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))))
77		sseq1 3626	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (𝑎 ⊆ 𝑏 ↔ (𝑢 “ {𝑞}) ⊆ 𝑏))
78	77	3anbi2d 1404	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋)))
79		eleq1 2689	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (𝑎 ∈ (𝑁‘𝑞) ↔ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)))
80	78, 79	anbi12d 747	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑢 “ {𝑞}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))))
81	80	imbi1d 331	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞))))
82		eleq1 2689	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ 𝑋 ↔ 𝑞 ∈ 𝑋))
83	82	anbi2d 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑞 → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ↔ (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋)))
84	83	3anbi1d 1403	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑞 → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋)))
85		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑞 → (𝑁‘𝑝) = (𝑁‘𝑞))
86	85	eleq2d 2687	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑞 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑎 ∈ (𝑁‘𝑞)))
87	84, 86	anbi12d 747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑞 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞))))
88	85	eleq2d 2687	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑞 → (𝑏 ∈ (𝑁‘𝑝) ↔ 𝑏 ∈ (𝑁‘𝑞)))
89	87, 88	imbi12d 334	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞))))
90	10	ustuqtop1 22045	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))
91	89, 90	chvarv 2263	. . . . . . . . . . . . . . 15 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞))
92	81, 91	vtoclg 3266	. . . . . . . . . . . . . 14 ⊢ ((𝑢 “ {𝑞}) ∈ V → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞)))
93	63, 92	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑈 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞)))
94	93	impcom 446	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → 𝑏 ∈ (𝑁‘𝑞))
95	76, 94	vtoclg 3266	. . . . . . . . . . 11 ⊢ ((𝑤 “ {𝑝}) ∈ V → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
96	69, 95	syl 17	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑈 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
97	96	impcom 446	. . . . . . . . 9 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
98	68, 56, 51, 97	syl21anc 1325	. . . . . . . 8 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
99	98	ralrimiva 2966	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
100		raleq 3138	. . . . . . . 8 ⊢ (𝑏 = (𝑢 “ {𝑝}) → (∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞) ↔ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
101	100	rspcev 3309	. . . . . . 7 ⊢ (((𝑢 “ {𝑝}) ∈ (𝑁‘𝑝) ∧ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
102	14, 99, 101	syl2anc 693	. . . . . 6 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
103		ustexhalf 22014	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑢 ∈ 𝑈 (𝑢 ∘ 𝑢) ⊆ 𝑤)
104	103	adantlr 751	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑢 ∈ 𝑈 (𝑢 ∘ 𝑢) ⊆ 𝑤)
105	102, 104	r19.29a 3078	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
106	105	adantr 481	. . . 4 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
107		eleq1 2689	. . . . . 6 ⊢ (𝑎 = (𝑤 “ {𝑝}) → (𝑎 ∈ (𝑁‘𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
108	107	rexralbidv 3058	. . . . 5 ⊢ (𝑎 = (𝑤 “ {𝑝}) → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
109	108	adantl 482	. . . 4 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
110	106, 109	mpbird 247	. . 3 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
111	110	adantllr 755	. 2 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
112		vex 3203	. . . 4 ⊢ 𝑎 ∈ V
113	10	ustuqtoplem 22043	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ V) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})))
114	112, 113	mpan2 707	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})))
115	114	biimpa 501	. 2 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝}))
116	111, 115	r19.29a 3078	1 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∃wex 1704 ∈ wcel 1990 ∀wral 2912 ∃wrex 2913 Vcvv 3200 ⊆ wss 3574 {csn 4177 class class class wbr 4653 ↦ cmpt 4729 ran crn 5115 “ cima 5117 ∘ ccom 5118 Rel wrel 5119 ‘cfv 5888 UnifOncust 22003

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-ust 22004

This theorem is referenced by: ustuqtop 22050 utopsnneiplem 22051

W3C validator