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 23396

Description: Lemma for ustuqtop 23398. (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 772	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋))
2		simplr 766	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → 𝑢 ∈ 𝑈)
3		eqid 2738	. . . . . . . . . . 11 ⊢ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})
4		imaeq1 5964	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑢 → (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
5	4	rspceeqv 3575	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ 𝑈 ∧ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
6	3, 5	mpan2 688	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑈 → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
7	6	adantl 482	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
8		imaexg 7762	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑈 → (𝑢 “ {𝑝}) ∈ V)
9		utopustuq.1	. . . . . . . . . . 11 ⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))
10	9	ustuqtoplem 23391	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑢 “ {𝑝}) ∈ V) → ((𝑢 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
11	8, 10	sylan2 593	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ((𝑢 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
12	7, 11	mpbird 256	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → (𝑢 “ {𝑝}) ∈ (𝑁‘𝑝))
13	1, 2, 12	syl2anc 584	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ∈ (𝑁‘𝑝))
14		simp-5l 782	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑈 ∈ (UnifOn‘𝑋))
15	1	simpld 495	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → 𝑈 ∈ (UnifOn‘𝑋))
16		simp-4r 781	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → 𝑝 ∈ 𝑋)
17		ustimasn 23380	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ 𝑝 ∈ 𝑋) → (𝑢 “ {𝑝}) ⊆ 𝑋)
18	15, 2, 16, 17	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ⊆ 𝑋)
19	18	sselda 3921	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑞 ∈ 𝑋)
20	14, 19	jca 512	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋))
21		simplr 766	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞 ∈ (𝑢 “ {𝑝}))
22		simp-6l 784	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑈 ∈ (UnifOn‘𝑋))
23		simp-4r 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑢 ∈ 𝑈)
24		ustrel 23363	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → Rel 𝑢)
25	22, 23, 24	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑢)
26		elrelimasn 5993	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel 𝑢 → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
27	25, 26	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
28	21, 27	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑢𝑞)
29		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑢 “ {𝑞}))
30		elrelimasn 5993	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel 𝑢 → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
31	25, 30	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
32	29, 31	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞𝑢𝑟)
33		vex 3436	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑝 ∈ V
34		vex 3436	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑟 ∈ V
35	33, 34	brco 5779	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝(𝑢 ∘ 𝑢)𝑟 ↔ ∃𝑞(𝑝𝑢𝑞 ∧ 𝑞𝑢𝑟))
36	35	biimpri 227	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑞(𝑝𝑢𝑞 ∧ 𝑞𝑢𝑟) → 𝑝(𝑢 ∘ 𝑢)𝑟)
37	36	19.23bi 2184	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝𝑢𝑞 ∧ 𝑞𝑢𝑟) → 𝑝(𝑢 ∘ 𝑢)𝑟)
38	28, 32, 37	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝(𝑢 ∘ 𝑢)𝑟)
39		simpllr 773	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑢 ∘ 𝑢) ⊆ 𝑤)
40	39	ssbrd 5117	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑝(𝑢 ∘ 𝑢)𝑟 → 𝑝𝑤𝑟))
41	38, 40	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑤𝑟)
42		simp-5r 783	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑤 ∈ 𝑈)
43		ustrel 23363	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈) → Rel 𝑤)
44	22, 42, 43	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑤)
45		elrelimasn 5993	. . . . . . . . . . . . . . 15 ⊢ (Rel 𝑤 → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
46	44, 45	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
47	41, 46	mpbird 256	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑤 “ {𝑝}))
48	47	ex 413	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑟 ∈ (𝑢 “ {𝑞}) → 𝑟 ∈ (𝑤 “ {𝑝})))
49	48	ssrdv 3927	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}))
50		simp-4r 781	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑤 ∈ 𝑈)
51	16	adantr 481	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑝 ∈ 𝑋)
52		ustimasn 23380	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈 ∧ 𝑝 ∈ 𝑋) → (𝑤 “ {𝑝}) ⊆ 𝑋)
53	14, 50, 51, 52	syl3anc 1370	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ⊆ 𝑋)
54	20, 49, 53	3jca 1127	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋))
55		simpllr 773	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑢 ∈ 𝑈)
56		eqidd 2739	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ 𝑈 → (𝑢 “ {𝑞}) = (𝑢 “ {𝑞}))
57		imaeq1 5964	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑢 → (𝑤 “ {𝑞}) = (𝑢 “ {𝑞}))
58	57	rspceeqv 3575	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ 𝑈 ∧ (𝑢 “ {𝑞}) = (𝑢 “ {𝑞})) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
59	56, 58	mpdan 684	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑈 → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
60	59	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
61		imaexg 7762	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑈 → (𝑢 “ {𝑞}) ∈ V)
62	9	ustuqtoplem 23391	. . . . . . . . . . . . 13 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ V) → ((𝑢 “ {𝑞}) ∈ (𝑁‘𝑞) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
63	61, 62	sylan2 593	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ((𝑢 “ {𝑞}) ∈ (𝑁‘𝑞) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
64	60, 63	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))
65	14, 19, 55, 64	syl21anc 835	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))
66	54, 65	jca 512	. . . . . . . . 9 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)))
67		imaexg 7762	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑈 → (𝑤 “ {𝑝}) ∈ V)
68		sseq2 3947	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((𝑢 “ {𝑞}) ⊆ 𝑏 ↔ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝})))
69		sseq1 3946	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ⊆ 𝑋 ↔ (𝑤 “ {𝑝}) ⊆ 𝑋))
70	68, 69	3anbi23d 1438	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋)))
71	70	anbi1d 630	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))))
72	71	anbi1d 630	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈)))
73		eleq1 2826	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ∈ (𝑁‘𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
74	72, 73	imbi12d 345	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → 𝑏 ∈ (𝑁‘𝑞)) ↔ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))))
75		sseq1 3946	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (𝑎 ⊆ 𝑏 ↔ (𝑢 “ {𝑞}) ⊆ 𝑏))
76	75	3anbi2d 1440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋)))
77		eleq1 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (𝑎 ∈ (𝑁‘𝑞) ↔ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)))
78	76, 77	anbi12d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑢 “ {𝑞}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))))
79	78	imbi1d 342	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞))))
80		eleq1 2826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ 𝑋 ↔ 𝑞 ∈ 𝑋))
81	80	anbi2d 629	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑞 → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ↔ (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋)))
82	81	3anbi1d 1439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑞 → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋)))
83		fveq2 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑞 → (𝑁‘𝑝) = (𝑁‘𝑞))
84	83	eleq2d 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑞 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑎 ∈ (𝑁‘𝑞)))
85	82, 84	anbi12d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑞 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞))))
86	83	eleq2d 2824	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑞 → (𝑏 ∈ (𝑁‘𝑝) ↔ 𝑏 ∈ (𝑁‘𝑞)))
87	85, 86	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞))))
88	9	ustuqtop1 23393	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))
89	87, 88	chvarvv 2002	. . . . . . . . . . . . . . 15 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞))
90	79, 89	vtoclg 3505	. . . . . . . . . . . . . 14 ⊢ ((𝑢 “ {𝑞}) ∈ V → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞)))
91	61, 90	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑈 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞)))
92	91	impcom 408	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → 𝑏 ∈ (𝑁‘𝑞))
93	74, 92	vtoclg 3505	. . . . . . . . . . 11 ⊢ ((𝑤 “ {𝑝}) ∈ V → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
94	67, 93	syl 17	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑈 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
95	94	impcom 408	. . . . . . . . 9 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
96	66, 55, 50, 95	syl21anc 835	. . . . . . . 8 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
97	96	ralrimiva 3103	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
98		raleq 3342	. . . . . . . 8 ⊢ (𝑏 = (𝑢 “ {𝑝}) → (∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞) ↔ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
99	98	rspcev 3561	. . . . . . 7 ⊢ (((𝑢 “ {𝑝}) ∈ (𝑁‘𝑝) ∧ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
100	13, 97, 99	syl2anc 584	. . . . . 6 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
101		ustexhalf 23362	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑢 ∈ 𝑈 (𝑢 ∘ 𝑢) ⊆ 𝑤)
102	101	adantlr 712	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑢 ∈ 𝑈 (𝑢 ∘ 𝑢) ⊆ 𝑤)
103	100, 102	r19.29a 3218	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
104	103	adantr 481	. . . 4 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
105		eleq1 2826	. . . . . 6 ⊢ (𝑎 = (𝑤 “ {𝑝}) → (𝑎 ∈ (𝑁‘𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
106	105	rexralbidv 3230	. . . . 5 ⊢ (𝑎 = (𝑤 “ {𝑝}) → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
107	106	adantl 482	. . . 4 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
108	104, 107	mpbird 256	. . 3 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
109	108	adantllr 716	. 2 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
110		vex 3436	. . . 4 ⊢ 𝑎 ∈ V
111	9	ustuqtoplem 23391	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ V) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})))
112	110, 111	mpan2 688	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})))
113	112	biimpa 477	. 2 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝}))
114	109, 113	r19.29a 3218	1 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∃wex 1782 ∈ wcel 2106 ∀wral 3064 ∃wrex 3065 Vcvv 3432 ⊆ wss 3887 {csn 4561 class class class wbr 5074 ↦ cmpt 5157 ran crn 5590 “ cima 5592 ∘ ccom 5593 Rel wrel 5594 ‘cfv 6433 UnifOncust 23351

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 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 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-ust 23352

This theorem is referenced by: ustuqtop 23398 utopsnneiplem 23399

W3C validator