Theorem restutop 24362

Description: Restriction of a topology induced by an uniform structure. (Contributed by Thierry Arnoux, 12-Dec-2017.)

Assertion

Ref	Expression
restutop	⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))))

Proof of Theorem restutop

Dummy variables 𝑎 𝑏 𝑢 𝑣 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 487	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋))
2		fvexd 6897	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (unifTop‘𝑈) ∈ V)
3		elfvex 6917	. . . . . . . . 9 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V)
4	3	adantr 485	. . . . . . . 8 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ V)
5		simpr 489	. . . . . . . 8 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋)
6	4, 5	ssexd 5295	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
7		elrest 17479	. . . . . . 7 ⊢ (((unifTop‘𝑈) ∈ V ∧ 𝐴 ∈ V) → (𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴) ↔ ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴)))
8	2, 6, 7	syl2anc 595	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴) ↔ ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴)))
9	8	biimpa 481	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) → ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴))
10		inss2 4198	. . . . . . 7 ⊢ (𝑎 ∩ 𝐴) ⊆ 𝐴
11		sseq1 3970	. . . . . . 7 ⊢ (𝑏 = (𝑎 ∩ 𝐴) → (𝑏 ⊆ 𝐴 ↔ (𝑎 ∩ 𝐴) ⊆ 𝐴))
12	10, 11	mpbiri 261	. . . . . 6 ⊢ (𝑏 = (𝑎 ∩ 𝐴) → 𝑏 ⊆ 𝐴)
13	12	rexlimivw 3168	. . . . 5 ⊢ (∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴) → 𝑏 ⊆ 𝐴)
14	9, 13	syl 18	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) → 𝑏 ⊆ 𝐴)
15		simp-5l 796	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑈 ∈ (UnifOn‘𝑋))
16	15	ad2antrr 738	. . . . . . . . 9 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → 𝑈 ∈ (UnifOn‘𝑋))
17	6	ad6antr 748	. . . . . . . . . 10 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → 𝐴 ∈ V)
18	17, 17	xpexd 7749	. . . . . . . . 9 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → (𝐴 × 𝐴) ∈ V)
19		simplr 780	. . . . . . . . 9 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → 𝑢 ∈ 𝑈)
20		elrestr 17480	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ 𝑢 ∈ 𝑈) → (𝑢 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
21	16, 18, 19, 20	syl3anc 1396	. . . . . . . 8 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → (𝑢 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
22		inss1 4197	. . . . . . . . . . . . 13 ⊢ (𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑢
23		imass1 6104	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑢 → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (𝑢 “ {𝑥}))
24	22, 23	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (𝑢 “ {𝑥})
25		sstr 3953	. . . . . . . . . . . 12 ⊢ ((((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (𝑢 “ {𝑥}) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝑎)
26	24, 25	mpan 702	. . . . . . . . . . 11 ⊢ ((𝑢 “ {𝑥}) ⊆ 𝑎 → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝑎)
27		imassrn 6074	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ ran (𝑢 ∩ (𝐴 × 𝐴))
28		rnin 6144	. . . . . . . . . . . . . . 15 ⊢ ran (𝑢 ∩ (𝐴 × 𝐴)) ⊆ (ran 𝑢 ∩ ran (𝐴 × 𝐴))
29	27, 28	sstri 3954	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (ran 𝑢 ∩ ran (𝐴 × 𝐴))
30		inss2 4198	. . . . . . . . . . . . . 14 ⊢ (ran 𝑢 ∩ ran (𝐴 × 𝐴)) ⊆ ran (𝐴 × 𝐴)
31	29, 30	sstri 3954	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ ran (𝐴 × 𝐴)
32		rnxpid 6172	. . . . . . . . . . . . 13 ⊢ ran (𝐴 × 𝐴) = 𝐴
33	31, 32	sseqtri 3993	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝐴
34	33	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑢 “ {𝑥}) ⊆ 𝑎 → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝐴)
35	26, 34	ssind 4201	. . . . . . . . . 10 ⊢ ((𝑢 “ {𝑥}) ⊆ 𝑎 → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (𝑎 ∩ 𝐴))
36	35	adantl 486	. . . . . . . . 9 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (𝑎 ∩ 𝐴))
37		simpllr 787	. . . . . . . . 9 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → 𝑏 = (𝑎 ∩ 𝐴))
38	36, 37	sseqtrrd 3982	. . . . . . . 8 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝑏)
39		imaeq1 6058	. . . . . . . . . 10 ⊢ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) → (𝑣 “ {𝑥}) = ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}))
40	39	sseq1d 3976	. . . . . . . . 9 ⊢ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) → ((𝑣 “ {𝑥}) ⊆ 𝑏 ↔ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝑏))
41	40	rspcev 3590	. . . . . . . 8 ⊢ (((𝑢 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝑏) → ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)
42	21, 38, 41	syl2anc 595	. . . . . . 7 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)
43		simplr 780	. . . . . . . 8 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑎 ∈ (unifTop‘𝑈))
44		simpllr 787	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑥 ∈ 𝑏)
45		simpr 489	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑏 = (𝑎 ∩ 𝐴))
46	44, 45	eleqtrd 2871	. . . . . . . . 9 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑥 ∈ (𝑎 ∩ 𝐴))
47	46	elin1d 4165	. . . . . . . 8 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑥 ∈ 𝑎)
48		elutop 24358	. . . . . . . . . 10 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑎 ∈ (unifTop‘𝑈) ↔ (𝑎 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝑎 ∃𝑢 ∈ 𝑈 (𝑢 “ {𝑥}) ⊆ 𝑎)))
49	48	simplbda 504	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ (unifTop‘𝑈)) → ∀𝑥 ∈ 𝑎 ∃𝑢 ∈ 𝑈 (𝑢 “ {𝑥}) ⊆ 𝑎)
50	49	r19.21bi 3263	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑥 ∈ 𝑎) → ∃𝑢 ∈ 𝑈 (𝑢 “ {𝑥}) ⊆ 𝑎)
51	15, 43, 47, 50	syl21anc 850	. . . . . . 7 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → ∃𝑢 ∈ 𝑈 (𝑢 “ {𝑥}) ⊆ 𝑎)
52	42, 51	r19.29a 3179	. . . . . 6 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)
53	9	adantr 485	. . . . . 6 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) → ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴))
54	52, 53	r19.29a 3179	. . . . 5 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) → ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)
55	54	ralrimiva 3163	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) → ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)
56		trust 24354	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))
57		elutop 24358	. . . . . 6 ⊢ ((𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴) → (𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))) ↔ (𝑏 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)))
58	56, 57	syl 18	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))) ↔ (𝑏 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)))
59	58	biimpar 482	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)) → 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))))
60	1, 14, 55, 59	syl12anc 849	. . 3 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) → 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))))
61	60	ex 417	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴) → 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))))
62	61	ssrdv 3951	1 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095  Vcvv 3463   ∩ cin 3912   ⊆ wss 3913  {csn 4594   × cxp 5660  ran crn 5663   “ cima 5665  ‘cfv 6537  (class class class)co 7411   ↾_t crest 17472  UnifOncust 24325  unifTopcutop 24355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7985  df-2nd 7986  df-rest 17474  df-ust 24326  df-utop 24356

This theorem is referenced by:  restutopopn  24363