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 24563

Description: Lemma for ustuqtop 24565. (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 787	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋))
2		simplr 781	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → 𝑢 ∈ 𝑈)
3		eqid 2760	. . . . . . . . . . 11 ⊢ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})
4		imaeq1 6046	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑢 → (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
5	4	rspceeqv 3598	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ 𝑈 ∧ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
6	3, 5	mpan2 704	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑈 → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
7	6	adantl 487	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
8		imaexg 7925	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑈 → (𝑢 “ {𝑝}) ∈ V)
9		utopustuq.1	. . . . . . . . . . 11 ⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))
10	9	ustuqtoplem 24558	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑢 “ {𝑝}) ∈ V) → ((𝑢 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
11	8, 10	sylan2 605	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ((𝑢 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
12	7, 11	mpbird 260	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → (𝑢 “ {𝑝}) ∈ (𝑁‘𝑝))
13	1, 2, 12	syl2anc 596	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ∈ (𝑁‘𝑝))
14		simp-5l 797	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑈 ∈ (UnifOn‘𝑋))
15	1	simpld 500	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → 𝑈 ∈ (UnifOn‘𝑋))
16		simp-4r 796	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → 𝑝 ∈ 𝑋)
17		ustimasn 24547	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ 𝑝 ∈ 𝑋) → (𝑢 “ {𝑝}) ⊆ 𝑋)
18	15, 2, 16, 17	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ⊆ 𝑋)
19	18	sselda 3908	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑞 ∈ 𝑋)
20	14, 19	jca 521	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋))
21		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞 ∈ (𝑢 “ {𝑝}))
22		simp-6l 799	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑈 ∈ (UnifOn‘𝑋))
23		simp-4r 796	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑢 ∈ 𝑈)
24		ustrel 24531	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → Rel 𝑢)
25	22, 23, 24	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑢)
26		elrelimasn 6083	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel 𝑢 → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
27	25, 26	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
28	21, 27	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑢𝑞)
29		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑢 “ {𝑞}))
30		elrelimasn 6083	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel 𝑢 → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
31	25, 30	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
32	29, 31	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞𝑢𝑟)
33		vex 3454	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑝 ∈ V
34		vex 3454	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑟 ∈ V
35	33, 34	brco 5847	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝(𝑢 ∘ 𝑢)𝑟 ↔ ∃𝑞(𝑝𝑢𝑞 ∧ 𝑞𝑢𝑟))
36	35	biimpri 231	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑞(𝑝𝑢𝑞 ∧ 𝑞𝑢𝑟) → 𝑝(𝑢 ∘ 𝑢)𝑟)
37	36	19.23bi 2227	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝𝑢𝑞 ∧ 𝑞𝑢𝑟) → 𝑝(𝑢 ∘ 𝑢)𝑟)
38	28, 32, 37	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝(𝑢 ∘ 𝑢)𝑟)
39		simpllr 788	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑢 ∘ 𝑢) ⊆ 𝑤)
40	39	ssbrd 5147	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑝(𝑢 ∘ 𝑢)𝑟 → 𝑝𝑤𝑟))
41	38, 40	mpd 16	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑤𝑟)
42		simp-5r 798	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑤 ∈ 𝑈)
43		ustrel 24531	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈) → Rel 𝑤)
44	22, 42, 43	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑤)
45		elrelimasn 6083	. . . . . . . . . . . . . . 15 ⊢ (Rel 𝑤 → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
46	44, 45	syl 18	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
47	41, 46	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑤 “ {𝑝}))
48	47	ex 418	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑟 ∈ (𝑢 “ {𝑞}) → 𝑟 ∈ (𝑤 “ {𝑝})))
49	48	ssrdv 3914	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}))
50		simp-4r 796	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑤 ∈ 𝑈)
51	16	adantr 486	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑝 ∈ 𝑋)
52		ustimasn 24547	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈 ∧ 𝑝 ∈ 𝑋) → (𝑤 “ {𝑝}) ⊆ 𝑋)
53	14, 50, 51, 52	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ⊆ 𝑋)
54	20, 49, 53	3jca 1146	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋))
55		simpllr 788	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑢 ∈ 𝑈)
56		eqidd 2761	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ 𝑈 → (𝑢 “ {𝑞}) = (𝑢 “ {𝑞}))
57		imaeq1 6046	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑢 → (𝑤 “ {𝑞}) = (𝑢 “ {𝑞}))
58	57	rspceeqv 3598	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ 𝑈 ∧ (𝑢 “ {𝑞}) = (𝑢 “ {𝑞})) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
59	56, 58	mpdan 700	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑈 → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
60	59	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
61		imaexg 7925	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑈 → (𝑢 “ {𝑞}) ∈ V)
62	9	ustuqtoplem 24558	. . . . . . . . . . . . 13 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ V) → ((𝑢 “ {𝑞}) ∈ (𝑁‘𝑞) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
63	61, 62	sylan2 605	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ((𝑢 “ {𝑞}) ∈ (𝑁‘𝑞) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
64	60, 63	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))
65	14, 19, 55, 64	syl21anc 851	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))
66	54, 65	jca 521	. . . . . . . . 9 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)))
67		imaexg 7925	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑈 → (𝑤 “ {𝑝}) ∈ V)
68		sseq2 3934	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((𝑢 “ {𝑞}) ⊆ 𝑏 ↔ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝})))
69		sseq1 3933	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ⊆ 𝑋 ↔ (𝑤 “ {𝑝}) ⊆ 𝑋))
70	68, 69	3anbi23d 1467	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋)))
71	70	anbi1d 643	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))))
72	71	anbi1d 643	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈)))
73		eleq1 2848	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ∈ (𝑁‘𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
74	72, 73	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → 𝑏 ∈ (𝑁‘𝑞)) ↔ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))))
75		sseq1 3933	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (𝑎 ⊆ 𝑏 ↔ (𝑢 “ {𝑞}) ⊆ 𝑏))
76	75	3anbi2d 1469	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋)))
77		eleq1 2848	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (𝑎 ∈ (𝑁‘𝑞) ↔ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)))
78	76, 77	anbi12d 644	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑢 “ {𝑞}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))))
79	78	imbi1d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞))))
80		eleq1 2848	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ 𝑋 ↔ 𝑞 ∈ 𝑋))
81	80	anbi2d 642	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑞 → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ↔ (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋)))
82	81	3anbi1d 1468	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑞 → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋)))
83		fveq2 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑞 → (𝑁‘𝑝) = (𝑁‘𝑞))
84	83	eleq2d 2846	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑞 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑎 ∈ (𝑁‘𝑞)))
85	82, 84	anbi12d 644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑞 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞))))
86	83	eleq2d 2846	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑞 → (𝑏 ∈ (𝑁‘𝑝) ↔ 𝑏 ∈ (𝑁‘𝑞)))
87	85, 86	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞))))
88	9	ustuqtop1 24560	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))
89	87, 88	chvarvv 2021	. . . . . . . . . . . . . . 15 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞))
90	79, 89	vtoclg 3517	. . . . . . . . . . . . . 14 ⊢ ((𝑢 “ {𝑞}) ∈ V → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞)))
91	61, 90	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑈 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞)))
92	91	impcom 413	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → 𝑏 ∈ (𝑁‘𝑞))
93	74, 92	vtoclg 3517	. . . . . . . . . . 11 ⊢ ((𝑤 “ {𝑝}) ∈ V → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
94	67, 93	syl 18	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑈 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
95	94	impcom 413	. . . . . . . . 9 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
96	66, 55, 50, 95	syl21anc 851	. . . . . . . 8 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
97	96	ralrimiva 3154	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
98		raleq 3316	. . . . . . . 8 ⊢ (𝑏 = (𝑢 “ {𝑝}) → (∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞) ↔ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
99	98	rspcev 3576	. . . . . . 7 ⊢ (((𝑢 “ {𝑝}) ∈ (𝑁‘𝑝) ∧ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
100	13, 97, 99	syl2anc 596	. . . . . 6 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
101		ustexhalf 24530	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑢 ∈ 𝑈 (𝑢 ∘ 𝑢) ⊆ 𝑤)
102	101	adantlr 728	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑢 ∈ 𝑈 (𝑢 ∘ 𝑢) ⊆ 𝑤)
103	100, 102	r19.29a 3170	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
104	103	adantr 486	. . . 4 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
105		eleq1 2848	. . . . . 6 ⊢ (𝑎 = (𝑤 “ {𝑝}) → (𝑎 ∈ (𝑁‘𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
106	105	rexralbidv 3228	. . . . 5 ⊢ (𝑎 = (𝑤 “ {𝑝}) → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
107	106	adantl 487	. . . 4 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
108	104, 107	mpbird 260	. . 3 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
109	108	adantllr 732	. 2 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
110		vex 3454	. . . 4 ⊢ 𝑎 ∈ V
111	9	ustuqtoplem 24558	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ V) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})))
112	110, 111	mpan2 704	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})))
113	112	biimpa 482	. 2 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝}))
114	109, 113	r19.29a 3170	1 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∃wex 1811 ∈ wcel 2144 ∀wral 3076 ∃wrex 3086 Vcvv 3450 ⊆ wss 3895 {csn 4583 class class class wbr 5102 ↦ cmpt 5185 ran crn 5651 “ cima 5653 ∘ ccom 5654 Rel wrel 5655 ‘cfv 6538 UnifOncust 24519

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-ust 24520

This theorem is used by: ustuqtop 24565 utopsnneiplem 24566

W3C validator