Theorem restutop 23389

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 483	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋))
2		fvexd 6789	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (unifTop‘𝑈) ∈ V)
3		elfvex 6807	. . . . . . . . 9 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V)
4	3	adantr 481	. . . . . . . 8 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ V)
5		simpr 485	. . . . . . . 8 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋)
6	4, 5	ssexd 5248	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V)
7		elrest 17138	. . . . . . 7 ⊢ (((unifTop‘𝑈) ∈ V ∧ 𝐴 ∈ V) → (𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴) ↔ ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴)))
8	2, 6, 7	syl2anc 584	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴) ↔ ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴)))
9	8	biimpa 477	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) → ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴))
10		inss2 4163	. . . . . . 7 ⊢ (𝑎 ∩ 𝐴) ⊆ 𝐴
11		sseq1 3946	. . . . . . 7 ⊢ (𝑏 = (𝑎 ∩ 𝐴) → (𝑏 ⊆ 𝐴 ↔ (𝑎 ∩ 𝐴) ⊆ 𝐴))
12	10, 11	mpbiri 257	. . . . . 6 ⊢ (𝑏 = (𝑎 ∩ 𝐴) → 𝑏 ⊆ 𝐴)
13	12	rexlimivw 3211	. . . . 5 ⊢ (∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴) → 𝑏 ⊆ 𝐴)
14	9, 13	syl 17	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) → 𝑏 ⊆ 𝐴)
15		simp-5l 782	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑈 ∈ (UnifOn‘𝑋))
16	15	ad2antrr 723	. . . . . . . . 9 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → 𝑈 ∈ (UnifOn‘𝑋))
17	6	ad6antr 733	. . . . . . . . . 10 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → 𝐴 ∈ V)
18	17, 17	xpexd 7601	. . . . . . . . 9 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → (𝐴 × 𝐴) ∈ V)
19		simplr 766	. . . . . . . . 9 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → 𝑢 ∈ 𝑈)
20		elrestr 17139	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ 𝑢 ∈ 𝑈) → (𝑢 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
21	16, 18, 19, 20	syl3anc 1370	. . . . . . . 8 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → (𝑢 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)))
22		inss1 4162	. . . . . . . . . . . . 13 ⊢ (𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑢
23		imass1 6009	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑢 → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (𝑢 “ {𝑥}))
24	22, 23	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (𝑢 “ {𝑥})
25		sstr 3929	. . . . . . . . . . . 12 ⊢ ((((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (𝑢 “ {𝑥}) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝑎)
26	24, 25	mpan 687	. . . . . . . . . . 11 ⊢ ((𝑢 “ {𝑥}) ⊆ 𝑎 → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝑎)
27		imassrn 5980	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ ran (𝑢 ∩ (𝐴 × 𝐴))
28		rnin 6050	. . . . . . . . . . . . . . 15 ⊢ ran (𝑢 ∩ (𝐴 × 𝐴)) ⊆ (ran 𝑢 ∩ ran (𝐴 × 𝐴))
29	27, 28	sstri 3930	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (ran 𝑢 ∩ ran (𝐴 × 𝐴))
30		inss2 4163	. . . . . . . . . . . . . 14 ⊢ (ran 𝑢 ∩ ran (𝐴 × 𝐴)) ⊆ ran (𝐴 × 𝐴)
31	29, 30	sstri 3930	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ ran (𝐴 × 𝐴)
32		rnxpid 6076	. . . . . . . . . . . . 13 ⊢ ran (𝐴 × 𝐴) = 𝐴
33	31, 32	sseqtri 3957	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝐴
34	33	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑢 “ {𝑥}) ⊆ 𝑎 → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝐴)
35	26, 34	ssind 4166	. . . . . . . . . 10 ⊢ ((𝑢 “ {𝑥}) ⊆ 𝑎 → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (𝑎 ∩ 𝐴))
36	35	adantl 482	. . . . . . . . 9 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ (𝑎 ∩ 𝐴))
37		simpllr 773	. . . . . . . . 9 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → 𝑏 = (𝑎 ∩ 𝐴))
38	36, 37	sseqtrrd 3962	. . . . . . . 8 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝑏)
39		imaeq1 5964	. . . . . . . . . 10 ⊢ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) → (𝑣 “ {𝑥}) = ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}))
40	39	sseq1d 3952	. . . . . . . . 9 ⊢ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) → ((𝑣 “ {𝑥}) ⊆ 𝑏 ↔ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝑏))
41	40	rspcev 3561	. . . . . . . 8 ⊢ (((𝑢 ∩ (𝐴 × 𝐴)) ∈ (𝑈 ↾t (𝐴 × 𝐴)) ∧ ((𝑢 ∩ (𝐴 × 𝐴)) “ {𝑥}) ⊆ 𝑏) → ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)
42	21, 38, 41	syl2anc 584	. . . . . . 7 ⊢ ((((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) ∧ 𝑢 ∈ 𝑈) ∧ (𝑢 “ {𝑥}) ⊆ 𝑎) → ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)
43		simplr 766	. . . . . . . 8 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑎 ∈ (unifTop‘𝑈))
44		simpllr 773	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑥 ∈ 𝑏)
45		simpr 485	. . . . . . . . . 10 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑏 = (𝑎 ∩ 𝐴))
46	44, 45	eleqtrd 2841	. . . . . . . . 9 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑥 ∈ (𝑎 ∩ 𝐴))
47	46	elin1d 4132	. . . . . . . 8 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → 𝑥 ∈ 𝑎)
48		elutop 23385	. . . . . . . . . 10 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑎 ∈ (unifTop‘𝑈) ↔ (𝑎 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝑎 ∃𝑢 ∈ 𝑈 (𝑢 “ {𝑥}) ⊆ 𝑎)))
49	48	simplbda 500	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ (unifTop‘𝑈)) → ∀𝑥 ∈ 𝑎 ∃𝑢 ∈ 𝑈 (𝑢 “ {𝑥}) ⊆ 𝑎)
50	49	r19.21bi 3134	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑥 ∈ 𝑎) → ∃𝑢 ∈ 𝑈 (𝑢 “ {𝑥}) ⊆ 𝑎)
51	15, 43, 47, 50	syl21anc 835	. . . . . . 7 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → ∃𝑢 ∈ 𝑈 (𝑢 “ {𝑥}) ⊆ 𝑎)
52	42, 51	r19.29a 3218	. . . . . 6 ⊢ ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) ∧ 𝑎 ∈ (unifTop‘𝑈)) ∧ 𝑏 = (𝑎 ∩ 𝐴)) → ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)
53	9	adantr 481	. . . . . 6 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) → ∃𝑎 ∈ (unifTop‘𝑈)𝑏 = (𝑎 ∩ 𝐴))
54	52, 53	r19.29a 3218	. . . . 5 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) ∧ 𝑥 ∈ 𝑏) → ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)
55	54	ralrimiva 3103	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) → ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)
56		trust 23381	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))
57		elutop 23385	. . . . . 6 ⊢ ((𝑈 ↾t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴) → (𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))) ↔ (𝑏 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)))
58	56, 57	syl 17	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))) ↔ (𝑏 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)))
59	58	biimpar 478	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ (𝑏 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑏 ∃𝑣 ∈ (𝑈 ↾t (𝐴 × 𝐴))(𝑣 “ {𝑥}) ⊆ 𝑏)) → 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))))
60	1, 14, 55, 59	syl12anc 834	. . 3 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴)) → 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))))
61	60	ex 413	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑏 ∈ ((unifTop‘𝑈) ↾t 𝐴) → 𝑏 ∈ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))))
62	61	ssrdv 3927	1 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065  Vcvv 3432   ∩ cin 3886   ⊆ wss 3887  {csn 4561   × cxp 5587  ran crn 5590   “ cima 5592  ‘cfv 6433  (class class class)co 7275   ↾_t crest 17131  UnifOncust 23351  unifTopcutop 23382

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-ov 7278  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832  df-rest 17133  df-ust 23352  df-utop 23383

This theorem is referenced by:  restutopopn  23390