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 21858

Description: Lemma for ustuqtop 21860. (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 794	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋))
2		simplr 788	. . . . . . . 8 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → 𝑢 ∈ 𝑈)
3		eqid 2610	. . . . . . . . . . 11 ⊢ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})
4		imaeq1 5380	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
5	4	eqeq2d 2620	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑢 → ((𝑢 “ {𝑝}) = (𝑤 “ {𝑝}) ↔ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})))
6	5	rspcev 3282	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ 𝑈 ∧ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
7	3, 6	mpan2 703	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑈 → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
8	7	adantl 481	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
9		imaexg 6995	. . . . . . . . . 10 ⊢ (𝑢 ∈ 𝑈 → (𝑢 “ {𝑝}) ∈ V)
10		utopustuq.1	. . . . . . . . . . 11 ⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))
11	10	ustuqtoplem 21853	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑢 “ {𝑝}) ∈ V) → ((𝑢 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
12	9, 11	sylan2 490	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ((𝑢 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
13	8, 12	mpbird 246	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → (𝑢 “ {𝑝}) ∈ (𝑁‘𝑝))
14	1, 2, 13	syl2anc 691	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ∈ (𝑁‘𝑝))
15		simp-5l 804	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑈 ∈ (UnifOn‘𝑋))
16	1	simpld 474	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → 𝑈 ∈ (UnifOn‘𝑋))
17		simp-4r 803	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → 𝑝 ∈ 𝑋)
18		ustimasn 21842	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈 ∧ 𝑝 ∈ 𝑋) → (𝑢 “ {𝑝}) ⊆ 𝑋)
19	16, 2, 17, 18	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ⊆ 𝑋)
20	19	sselda 3568	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑞 ∈ 𝑋)
21	15, 20	jca 553	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋))
22		simplr 788	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞 ∈ (𝑢 “ {𝑝}))
23		simp-6l 806	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑈 ∈ (UnifOn‘𝑋))
24		simp-4r 803	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑢 ∈ 𝑈)
25		ustrel 21825	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢 ∈ 𝑈) → Rel 𝑢)
26	23, 24, 25	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑢)
27		elrelimasn 5408	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel 𝑢 → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
28	26, 27	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
29	22, 28	mpbid 221	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑢𝑞)
30		simpr 476	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑢 “ {𝑞}))
31		elrelimasn 5408	. . . . . . . . . . . . . . . . . 18 ⊢ (Rel 𝑢 → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
32	26, 31	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
33	30, 32	mpbid 221	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞𝑢𝑟)
34		vex 3176	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑝 ∈ V
35		vex 3176	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑟 ∈ V
36	34, 35	brco 5214	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝(𝑢 ∘ 𝑢)𝑟 ↔ ∃𝑞(𝑝𝑢𝑞 ∧ 𝑞𝑢𝑟))
37	36	biimpri 217	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑞(𝑝𝑢𝑞 ∧ 𝑞𝑢𝑟) → 𝑝(𝑢 ∘ 𝑢)𝑟)
38	37	19.23bi 2049	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝𝑢𝑞 ∧ 𝑞𝑢𝑟) → 𝑝(𝑢 ∘ 𝑢)𝑟)
39	29, 33, 38	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝(𝑢 ∘ 𝑢)𝑟)
40		simpllr 795	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑢 ∘ 𝑢) ⊆ 𝑤)
41	40	ssbrd 4626	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑝(𝑢 ∘ 𝑢)𝑟 → 𝑝𝑤𝑟))
42	39, 41	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑤𝑟)
43		simp-5r 805	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑤 ∈ 𝑈)
44		ustrel 21825	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈) → Rel 𝑤)
45	23, 43, 44	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑤)
46		elrelimasn 5408	. . . . . . . . . . . . . . 15 ⊢ (Rel 𝑤 → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
47	45, 46	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
48	42, 47	mpbird 246	. . . . . . . . . . . . 13 ⊢ (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑤 “ {𝑝}))
49	48	ex 449	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑟 ∈ (𝑢 “ {𝑞}) → 𝑟 ∈ (𝑤 “ {𝑝})))
50	49	ssrdv 3574	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}))
51		simp-4r 803	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑤 ∈ 𝑈)
52	17	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑝 ∈ 𝑋)
53		ustimasn 21842	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈 ∧ 𝑝 ∈ 𝑋) → (𝑤 “ {𝑝}) ⊆ 𝑋)
54	15, 51, 52, 53	syl3anc 1318	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ⊆ 𝑋)
55	21, 50, 54	3jca 1235	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋))
56		simpllr 795	. . . . . . . . . . 11 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑢 ∈ 𝑈)
57		eqidd 2611	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ 𝑈 → (𝑢 “ {𝑞}) = (𝑢 “ {𝑞}))
58		imaeq1 5380	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑢 → (𝑤 “ {𝑞}) = (𝑢 “ {𝑞}))
59	58	eqeq2d 2620	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑢 → ((𝑢 “ {𝑞}) = (𝑤 “ {𝑞}) ↔ (𝑢 “ {𝑞}) = (𝑢 “ {𝑞})))
60	59	rspcev 3282	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ 𝑈 ∧ (𝑢 “ {𝑞}) = (𝑢 “ {𝑞})) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
61	57, 60	mpdan 699	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑈 → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
62	61	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
63		imaexg 6995	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑈 → (𝑢 “ {𝑞}) ∈ V)
64	10	ustuqtoplem 21853	. . . . . . . . . . . . 13 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ V) → ((𝑢 “ {𝑞}) ∈ (𝑁‘𝑞) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
65	63, 64	sylan2 490	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → ((𝑢 “ {𝑞}) ∈ (𝑁‘𝑞) ↔ ∃𝑤 ∈ 𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
66	62, 65	mpbird 246	. . . . . . . . . . 11 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑢 ∈ 𝑈) → (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))
67	15, 20, 56, 66	syl21anc 1317	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))
68	55, 67	jca 553	. . . . . . . . 9 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)))
69		imaexg 6995	. . . . . . . . . . 11 ⊢ (𝑤 ∈ 𝑈 → (𝑤 “ {𝑝}) ∈ V)
70		sseq2 3590	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((𝑢 “ {𝑞}) ⊆ 𝑏 ↔ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝})))
71		sseq1 3589	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ⊆ 𝑋 ↔ (𝑤 “ {𝑝}) ⊆ 𝑋))
72	70, 71	3anbi23d 1394	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋)))
73	72	anbi1d 737	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))))
74	73	anbi1d 737	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈)))
75		eleq1 2676	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ∈ (𝑁‘𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
76	74, 75	imbi12d 333	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑤 “ {𝑝}) → ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → 𝑏 ∈ (𝑁‘𝑞)) ↔ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))))
77		sseq1 3589	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (𝑎 ⊆ 𝑏 ↔ (𝑢 “ {𝑞}) ⊆ 𝑏))
78	77	3anbi2d 1396	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋)))
79		eleq1 2676	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (𝑎 ∈ (𝑁‘𝑞) ↔ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)))
80	78, 79	anbi12d 743	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = (𝑢 “ {𝑞}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞))))
81	80	imbi1d 330	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = (𝑢 “ {𝑞}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞))))
82		eleq1 2676	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ 𝑋 ↔ 𝑞 ∈ 𝑋))
83	82	anbi2d 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑞 → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ↔ (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋)))
84	83	3anbi1d 1395	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑞 → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋)))
85		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑞 → (𝑁‘𝑝) = (𝑁‘𝑞))
86	85	eleq2d 2673	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑞 → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑎 ∈ (𝑁‘𝑞)))
87	84, 86	anbi12d 743	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑞 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞))))
88	85	eleq2d 2673	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑞 → (𝑏 ∈ (𝑁‘𝑝) ↔ 𝑏 ∈ (𝑁‘𝑞)))
89	87, 88	imbi12d 333	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞))))
90	10	ustuqtop1 21855	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))
91	89, 90	chvarv 2251	. . . . . . . . . . . . . . 15 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞))
92	81, 91	vtoclg 3239	. . . . . . . . . . . . . 14 ⊢ ((𝑢 “ {𝑞}) ∈ V → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞)))
93	63, 92	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑈 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) → 𝑏 ∈ (𝑁‘𝑞)))
94	93	impcom 445	. . . . . . . . . . . 12 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → 𝑏 ∈ (𝑁‘𝑞))
95	76, 94	vtoclg 3239	. . . . . . . . . . 11 ⊢ ((𝑤 “ {𝑝}) ∈ V → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
96	69, 95	syl 17	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑈 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
97	96	impcom 445	. . . . . . . . 9 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞 ∈ 𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁‘𝑞)) ∧ 𝑢 ∈ 𝑈) ∧ 𝑤 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
98	68, 56, 51, 97	syl21anc 1317	. . . . . . . 8 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
99	98	ralrimiva 2949	. . . . . . 7 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
100		raleq 3115	. . . . . . . 8 ⊢ (𝑏 = (𝑢 “ {𝑝}) → (∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞) ↔ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
101	100	rspcev 3282	. . . . . . 7 ⊢ (((𝑢 “ {𝑝}) ∈ (𝑁‘𝑝) ∧ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
102	14, 99, 101	syl2anc 691	. . . . . 6 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 ∘ 𝑢) ⊆ 𝑤) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
103		ustexhalf 21824	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑢 ∈ 𝑈 (𝑢 ∘ 𝑢) ⊆ 𝑤)
104	103	adantlr 747	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑢 ∈ 𝑈 (𝑢 ∘ 𝑢) ⊆ 𝑤)
105	102, 104	r19.29a 3060	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
106	105	adantr 480	. . . 4 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞))
107		eleq1 2676	. . . . . 6 ⊢ (𝑎 = (𝑤 “ {𝑝}) → (𝑎 ∈ (𝑁‘𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
108	107	rexralbidv 3040	. . . . 5 ⊢ (𝑎 = (𝑤 “ {𝑝}) → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
109	108	adantl 481	. . . 4 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞) ↔ ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 (𝑤 “ {𝑝}) ∈ (𝑁‘𝑞)))
110	106, 109	mpbird 246	. . 3 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
111	110	adantllr 751	. 2 ⊢ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) ∧ 𝑤 ∈ 𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))
112		vex 3176	. . . 4 ⊢ 𝑎 ∈ V
113	10	ustuqtoplem 21853	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ V) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})))
114	112, 113	mpan2 703	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝})))
115	114	biimpa 500	. 2 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑤 ∈ 𝑈 𝑎 = (𝑤 “ {𝑝}))
116	111, 115	r19.29a 3060	1 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∃wex 1695 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 Vcvv 3173 ⊆ wss 3540 {csn 4125 class class class wbr 4583 ↦ cmpt 4643 ran crn 5039 “ cima 5041 ∘ ccom 5042 Rel wrel 5043 ‘cfv 5804 UnifOncust 21813

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-ust 21814

This theorem is referenced by: ustuqtop 21860 utopsnneiplem 21861

W3C validator