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 22850

Description: Lemma for ustuqtop 22852. (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 774	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋))
2		simplr 768	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → 𝑢 ∈ 𝑈)
3		eqid 2798	. . . . . . . . . . 11 ⊢ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})
4		imaeq1 5891	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑢 → (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
5	4	rspceeqv 3586	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ 𝑈 ∧ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
6	3, 5	mpan2 690	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑈 → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
7	6	adantl 485	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
8		imaexg 7602	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑈 → (𝑢 “ {𝑝}) ∈ V)
9		utopustuq.1	. . . . . . . . . . 11 ⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))
10	9	ustuqtoplem 22845	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑢 “ {𝑝}) ∈ V) → ((𝑢 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
11	8, 10	sylan2 595	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ((𝑢 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
12	7, 11	mpbird 260	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → (𝑢 “ {𝑝}) ∈ (𝑁‘𝑝))
13	1, 2, 12	syl2anc 587	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ∈ (𝑁‘𝑝))
14		simp-5l 784	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑈 ∈ (UnifOn‘𝑋))
15	1	simpld 498	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → 𝑈 ∈ (UnifOn‘𝑋))
16		simp-4r 783	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → 𝑝 ∈ 𝑋)
17		ustimasn 22834	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ 𝑝 ∈ 𝑋) → (𝑢 “ {𝑝}) ⊆ 𝑋)
18	15, 2, 16, 17	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ⊆ 𝑋)
19	18	sselda 3915	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑞 ∈ 𝑋)
20	14, 19	jca 515	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋))
21		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞 ∈ (𝑢 “ {𝑝}))
22		simp-6l 786	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑈 ∈ (UnifOn‘𝑋))
23		simp-4r 783	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑢 ∈ 𝑈)
24		ustrel 22817	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → Rel 𝑢)
25	22, 23, 24	syl2anc 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑢)
26		elrelimasn 5920	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel 𝑢 → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
27	25, 26	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
28	21, 27	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑢𝑞)
29		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑢 “ {𝑞}))
30		elrelimasn 5920	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel 𝑢 → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
31	25, 30	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
32	29, 31	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞𝑢𝑟)
33		vex 3444	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑝 ∈ V
34		vex 3444	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑟 ∈ V
35	33, 34	brco 5705	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝(𝑢 ∘ 𝑢)𝑟 ↔ ∃𝑞(𝑝𝑢𝑞 ∧ 𝑞𝑢𝑟))
36	35	biimpri 231	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑞(𝑝𝑢𝑞 ∧ 𝑞𝑢𝑟) → 𝑝(𝑢 ∘ 𝑢)𝑟)
37	36	19.23bi 2188	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝𝑢𝑞 ∧ 𝑞𝑢𝑟) → 𝑝(𝑢 ∘ 𝑢)𝑟)
38	28, 32, 37	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝(𝑢 ∘ 𝑢)𝑟)
39		simpllr 775	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑢 ∘ 𝑢) ⊆ 𝑤)
40	39	ssbrd 5073	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑝(𝑢 ∘ 𝑢)𝑟 → 𝑝𝑤𝑟))
41	38, 40	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑤𝑟)
42		simp-5r 785	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑤 ∈ 𝑈)
43		ustrel 22817	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈) → Rel 𝑤)
44	22, 42, 43	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑤)
45		elrelimasn 5920	. . . . . . . . . . . . . . 15 ⊢ (Rel 𝑤 → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
46	44, 45	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
47	41, 46	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑤 “ {𝑝}))
48	47	ex 416	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑟 ∈ (𝑢 “ {𝑞}) → 𝑟 ∈ (𝑤 “ {𝑝})))
49	48	ssrdv 3921	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}))
50		simp-4r 783	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑤 ∈ 𝑈)
51	16	adantr 484	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑝 ∈ 𝑋)
52		ustimasn 22834	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈 ∧ 𝑝 ∈ 𝑋) → (𝑤 “ {𝑝}) ⊆ 𝑋)
53	14, 50, 51, 52	syl3anc 1368	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ⊆ 𝑋)
54	20, 49, 53	3jca 1125	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋))
55		simpllr 775	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑢 ∈ 𝑈)
56		eqidd 2799	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ 𝑈 → (𝑢 “ {𝑞}) = (𝑢 “ {𝑞}))
57		imaeq1 5891	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑢 → (𝑤 “ {𝑞}) = (𝑢 “ {𝑞}))
58	57	rspceeqv 3586	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ 𝑈 ∧ (𝑢 “ {𝑞}) = (𝑢 “ {𝑞})) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
59	56, 58	mpdan 686	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑈 → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
60	59	adantl 485	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
61		imaexg 7602	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑈 → (𝑢 “ {𝑞}) ∈ V)
62	9	ustuqtoplem 22845	. . . . . . . . . . . . 13 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ V) → ((𝑢 “ {𝑞}) ∈ (𝑁‘𝑞) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
63	61, 62	sylan2 595	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ((𝑢 “ {𝑞}) ∈ (𝑁‘𝑞) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
64	60, 63	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))
65	14, 19, 55, 64	syl21anc 836	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))
66	54, 65	jca 515	. . . . . . . . 9 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)))
67		imaexg 7602	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑈 → (𝑤 “ {𝑝}) ∈ V)
68		sseq2 3941	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((𝑢 “ {𝑞}) ⊆ 𝑏 ↔ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝})))
69		sseq1 3940	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ⊆ 𝑋 ↔ (𝑤 “ {𝑝}) ⊆ 𝑋))
70	68, 69	3anbi23d 1436	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋)))
71	70	anbi1d 632	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))))
72	71	anbi1d 632	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈)))
73		eleq1 2877	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ∈ (𝑁‘𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
74	72, 73	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → 𝑏 ∈ (𝑁‘𝑞)) ↔ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))))
75		sseq1 3940	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (𝑎 ⊆ 𝑏 ↔ (𝑢 “ {𝑞}) ⊆ 𝑏))
76	75	3anbi2d 1438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋)))
77		eleq1 2877	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (𝑎 ∈ (𝑁‘𝑞) ↔ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)))
78	76, 77	anbi12d 633	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑢 “ {𝑞}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))))
79	78	imbi1d 345	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞))))
80		eleq1 2877	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ 𝑋 ↔ 𝑞 ∈ 𝑋))
81	80	anbi2d 631	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑞 → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ↔ (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋)))
82	81	3anbi1d 1437	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑞 → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋)))
83		fveq2 6645	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑞 → (𝑁‘𝑝) = (𝑁‘𝑞))
84	83	eleq2d 2875	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑞 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑎 ∈ (𝑁‘𝑞)))
85	82, 84	anbi12d 633	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑞 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞))))
86	83	eleq2d 2875	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑞 → (𝑏 ∈ (𝑁‘𝑝) ↔ 𝑏 ∈ (𝑁‘𝑞)))
87	85, 86	imbi12d 348	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞))))
88	9	ustuqtop1 22847	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))
89	87, 88	chvarvv 2005	. . . . . . . . . . . . . . 15 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞))
90	79, 89	vtoclg 3515	. . . . . . . . . . . . . 14 ⊢ ((𝑢 “ {𝑞}) ∈ V → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞)))
91	61, 90	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑈 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞)))
92	91	impcom 411	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → 𝑏 ∈ (𝑁‘𝑞))
93	74, 92	vtoclg 3515	. . . . . . . . . . 11 ⊢ ((𝑤 “ {𝑝}) ∈ V → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
94	67, 93	syl 17	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑈 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
95	94	impcom 411	. . . . . . . . 9 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
96	66, 55, 50, 95	syl21anc 836	. . . . . . . 8 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
97	96	ralrimiva 3149	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
98		raleq 3358	. . . . . . . 8 ⊢ (𝑏 = (𝑢 “ {𝑝}) → (∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞) ↔ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
99	98	rspcev 3571	. . . . . . 7 ⊢ (((𝑢 “ {𝑝}) ∈ (𝑁‘𝑝) ∧ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
100	13, 97, 99	syl2anc 587	. . . . . 6 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
101		ustexhalf 22816	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑢 ∈ 𝑈 (𝑢 ∘ 𝑢) ⊆ 𝑤)
102	101	adantlr 714	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑢 ∈ 𝑈 (𝑢 ∘ 𝑢) ⊆ 𝑤)
103	100, 102	r19.29a 3248	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
104	103	adantr 484	. . . 4 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
105		eleq1 2877	. . . . . 6 ⊢ (𝑎 = (𝑤 “ {𝑝}) → (𝑎 ∈ (𝑁‘𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
106	105	rexralbidv 3260	. . . . 5 ⊢ (𝑎 = (𝑤 “ {𝑝}) → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
107	106	adantl 485	. . . 4 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
108	104, 107	mpbird 260	. . 3 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
109	108	adantllr 718	. 2 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
110		vex 3444	. . . 4 ⊢ 𝑎 ∈ V
111	9	ustuqtoplem 22845	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ V) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})))
112	110, 111	mpan2 690	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})))
113	112	biimpa 480	. 2 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝}))
114	109, 113	r19.29a 3248	1 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∃wex 1781 ∈ wcel 2111 ∀wral 3106 ∃wrex 3107 Vcvv 3441 ⊆ wss 3881 {csn 4525 class class class wbr 5030 ↦ cmpt 5110 ran crn 5520 “ cima 5522 ∘ ccom 5523 Rel wrel 5524 ‘cfv 6324 UnifOncust 22805

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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-reu 3113 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-ust 22806

This theorem is referenced by: ustuqtop 22852 utopsnneiplem 22853

W3C validator