Theorem fmucnd 23143

Description: The image of a Cauchy filter base by an uniformly continuous function is a Cauchy filter base. Deduction form. Proposition 3 of [BourbakiTop1] p. II.13. (Contributed by Thierry Arnoux, 18-Nov-2017.)

Hypotheses

Ref	Expression
fmucnd.1	⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))
fmucnd.2	⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))
fmucnd.3	⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))
fmucnd.4	⊢ (𝜑 → 𝐶 ∈ (CauFilu‘𝑈))
fmucnd.5	⊢ 𝐷 = ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎))

Assertion

Ref	Expression
fmucnd	⊢ (𝜑 → 𝐷 ∈ (CauFilu‘𝑉))

Distinct variable groups:   𝐶,𝑎   𝐷,𝑎   𝐹,𝑎   𝑉,𝑎   𝑋,𝑎   𝑌,𝑎   𝜑,𝑎

Allowed substitution hint:   𝑈(𝑎)

Proof of Theorem fmucnd

Dummy variables 𝑐 𝑏 𝑣 𝑟 𝑠 𝑡 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fmucnd.1	. . . 4 ⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋))
2		fmucnd.4	. . . 4 ⊢ (𝜑 → 𝐶 ∈ (CauFilu‘𝑈))
3		cfilufbas 23140	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈)) → 𝐶 ∈ (fBas‘𝑋))
4	1, 2, 3	syl2anc 587	. . 3 ⊢ (𝜑 → 𝐶 ∈ (fBas‘𝑋))
5		fmucnd.2	. . . 4 ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))
6		fmucnd.3	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))
7		isucn 23129	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)))))
8	7	simprbda 502	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) ∧ 𝐹 ∈ (𝑈 Cnu𝑉)) → 𝐹:𝑋⟶𝑌)
9	1, 5, 6, 8	syl21anc 838	. . 3 ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)
10	5	elfvexd 6729	. . 3 ⊢ (𝜑 → 𝑌 ∈ V)
11		fmucnd.5	. . . 4 ⊢ 𝐷 = ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎))
12	11	fbasrn 22735	. . 3 ⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ V) → 𝐷 ∈ (fBas‘𝑌))
13	4, 9, 10, 12	syl3anc 1373	. 2 ⊢ (𝜑 → 𝐷 ∈ (fBas‘𝑌))
14		simplr 769	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → 𝑎 ∈ 𝐶)
15		eqid 2736	. . . . . . . 8 ⊢ (𝐹 “ 𝑎) = (𝐹 “ 𝑎)
16		imaeq2 5910	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → (𝐹 “ 𝑐) = (𝐹 “ 𝑎))
17	16	rspceeqv 3542	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐶 ∧ (𝐹 “ 𝑎) = (𝐹 “ 𝑎)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))
18	14, 15, 17	sylancl 589	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))
19		imaexg 7671	. . . . . . . . 9 ⊢ (𝐹 ∈ (𝑈 Cnu𝑉) → (𝐹 “ 𝑎) ∈ V)
20		eqid 2736	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
21	20	elrnmpt 5810	. . . . . . . . 9 ⊢ ((𝐹 “ 𝑎) ∈ V → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)))
22	6, 19, 21	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)))
23	22	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)))
24	18, 23	mpbird 260	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → (𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)))
25		imaeq2 5910	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝐹 “ 𝑎) = (𝐹 “ 𝑐))
26	25	cbvmptv 5143	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
27	26	rneqi 5791	. . . . . . 7 ⊢ ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
28	11, 27	eqtri 2759	. . . . . 6 ⊢ 𝐷 = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
29	24, 28	eleqtrrdi 2842	. . . . 5 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → (𝐹 “ 𝑎) ∈ 𝐷)
30	9	ffnd 6524	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn 𝑋)
31	30	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → 𝐹 Fn 𝑋)
32		fbelss 22684	. . . . . . . . 9 ⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋)
33	4, 32	sylan 583	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋)
34	33	ad4ant13 751	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → 𝑎 ⊆ 𝑋)
35		fmucndlem 23142	. . . . . . 7 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑎 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)))
36	31, 34, 35	syl2anc 587	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)))
37		eqid 2736	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
38	37	mpofun 7312	. . . . . . . 8 ⊢ Fun (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
39		funimass2 6441	. . . . . . . 8 ⊢ ((Fun (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
40	38, 39	mpan 690	. . . . . . 7 ⊢ ((𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
41	40	adantl 485	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
42	36, 41	eqsstrrd 3926	. . . . 5 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣)
43		id 22	. . . . . . . 8 ⊢ (𝑏 = (𝐹 “ 𝑎) → 𝑏 = (𝐹 “ 𝑎))
44	43	sqxpeqd 5568	. . . . . . 7 ⊢ (𝑏 = (𝐹 “ 𝑎) → (𝑏 × 𝑏) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)))
45	44	sseq1d 3918	. . . . . 6 ⊢ (𝑏 = (𝐹 “ 𝑎) → ((𝑏 × 𝑏) ⊆ 𝑣 ↔ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣))
46	45	rspcev 3527	. . . . 5 ⊢ (((𝐹 “ 𝑎) ∈ 𝐷 ∧ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
47	29, 42, 46	syl2anc 587	. . . 4 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
48	1	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑈 ∈ (UnifOn‘𝑋))
49	2	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝐶 ∈ (CauFilu‘𝑈))
50	5	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑉 ∈ (UnifOn‘𝑌))
51	6	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝐹 ∈ (𝑈 Cnu𝑉))
52		simpr 488	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉)
53		nfcv 2897	. . . . . . 7 ⊢ Ⅎ𝑠⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩
54		nfcv 2897	. . . . . . 7 ⊢ Ⅎ𝑡⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩
55		nfcv 2897	. . . . . . 7 ⊢ Ⅎ𝑥⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩
56		nfcv 2897	. . . . . . 7 ⊢ Ⅎ𝑦⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩
57		simpl 486	. . . . . . . . 9 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑥 = 𝑠)
58	57	fveq2d 6699	. . . . . . . 8 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑥) = (𝐹‘𝑠))
59		simpr 488	. . . . . . . . 9 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑦 = 𝑡)
60	59	fveq2d 6699	. . . . . . . 8 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑦) = (𝐹‘𝑡))
61	58, 60	opeq12d 4778	. . . . . . 7 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ = ⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩)
62	53, 54, 55, 56, 61	cbvmpo 7283	. . . . . 6 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) = (𝑠 ∈ 𝑋, 𝑡 ∈ 𝑋 ↦ ⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩)
63	48, 50, 51, 52, 62	ucnprima 23133	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣) ∈ 𝑈)
64		cfiluexsm 23141	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈) ∧ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣) ∈ 𝑈) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣))
65	48, 49, 63, 64	syl3anc 1373	. . . 4 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣))
66	47, 65	r19.29a 3198	. . 3 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
67	66	ralrimiva 3095	. 2 ⊢ (𝜑 → ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
68		iscfilu 23139	. . 3 ⊢ (𝑉 ∈ (UnifOn‘𝑌) → (𝐷 ∈ (CauFilu‘𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)))
69	5, 68	syl 17	. 2 ⊢ (𝜑 → (𝐷 ∈ (CauFilu‘𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)))
70	13, 67, 69	mpbir2and 713	1 ⊢ (𝜑 → 𝐷 ∈ (CauFilu‘𝑉))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2112  ∀wral 3051  ∃wrex 3052  Vcvv 3398   ⊆ wss 3853  ⟨cop 4533   class class class wbr 5039   ↦ cmpt 5120   × cxp 5534  ^◡ccnv 5535  ran crn 5537   “ cima 5539  Fun wfun 6352   Fn wfn 6353  ⟶wf 6354  ‘cfv 6358  (class class class)co 7191   ∈ cmpo 7193  fBascfbas 20305  UnifOncust 23051   Cn_ucucn 23126  CauFil_uccfilu 23137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-rep 5164  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-fv 6366  df-ov 7194  df-oprab 7195  df-mpo 7196  df-1st 7739  df-2nd 7740  df-map 8488  df-fbas 20314  df-ust 23052  df-ucn 23127  df-cfilu 23138

This theorem is referenced by:  ucnextcn  23155