Theorem fmucnd 24256

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 24253	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈)) → 𝐶 ∈ (fBas‘𝑋))
4	1, 2, 3	syl2anc 585	. . 3 ⊢ (𝜑 → 𝐶 ∈ (fBas‘𝑋))
5		fmucnd.2	. . . 4 ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))
6		fmucnd.3	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))
7		isucn 24242	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)))))
8	7	simprbda 498	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) ∧ 𝐹 ∈ (𝑈 Cnu𝑉)) → 𝐹:𝑋⟶𝑌)
9	1, 5, 6, 8	syl21anc 838	. . 3 ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)
10	5	elfvexd 6876	. . 3 ⊢ (𝜑 → 𝑌 ∈ V)
11		fmucnd.5	. . . 4 ⊢ 𝐷 = ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎))
12	11	fbasrn 23849	. . 3 ⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ V) → 𝐷 ∈ (fBas‘𝑌))
13	4, 9, 10, 12	syl3anc 1374	. 2 ⊢ (𝜑 → 𝐷 ∈ (fBas‘𝑌))
14		simplr 769	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → 𝑎 ∈ 𝐶)
15		eqid 2736	. . . . . . . 8 ⊢ (𝐹 “ 𝑎) = (𝐹 “ 𝑎)
16		imaeq2 6021	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → (𝐹 “ 𝑐) = (𝐹 “ 𝑎))
17	16	rspceeqv 3587	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐶 ∧ (𝐹 “ 𝑎) = (𝐹 “ 𝑎)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))
18	14, 15, 17	sylancl 587	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))
19		imaexg 7864	. . . . . . . . 9 ⊢ (𝐹 ∈ (𝑈 Cnu𝑉) → (𝐹 “ 𝑎) ∈ V)
20		eqid 2736	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
21	20	elrnmpt 5913	. . . . . . . . 9 ⊢ ((𝐹 “ 𝑎) ∈ V → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)))
22	6, 19, 21	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)))
23	22	ad3antrrr 731	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)))
24	18, 23	mpbird 257	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → (𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)))
25		imaeq2 6021	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝐹 “ 𝑎) = (𝐹 “ 𝑐))
26	25	cbvmptv 5189	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
27	26	rneqi 5892	. . . . . . 7 ⊢ ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
28	11, 27	eqtri 2759	. . . . . 6 ⊢ 𝐷 = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
29	24, 28	eleqtrrdi 2847	. . . . 5 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → (𝐹 “ 𝑎) ∈ 𝐷)
30	9	ffnd 6669	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn 𝑋)
31	30	ad3antrrr 731	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → 𝐹 Fn 𝑋)
32		fbelss 23798	. . . . . . . . 9 ⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋)
33	4, 32	sylan 581	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋)
34	33	ad4ant13 752	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → 𝑎 ⊆ 𝑋)
35		fmucndlem 24255	. . . . . . 7 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑎 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)))
36	31, 34, 35	syl2anc 585	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)))
37		eqid 2736	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
38	37	mpofun 7491	. . . . . . . 8 ⊢ Fun (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
39		funimass2 6581	. . . . . . . 8 ⊢ ((Fun (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
40	38, 39	mpan 691	. . . . . . 7 ⊢ ((𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
41	40	adantl 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
42	36, 41	eqsstrrd 3957	. . . . 5 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣)
43		id 22	. . . . . . . 8 ⊢ (𝑏 = (𝐹 “ 𝑎) → 𝑏 = (𝐹 “ 𝑎))
44	43	sqxpeqd 5663	. . . . . . 7 ⊢ (𝑏 = (𝐹 “ 𝑎) → (𝑏 × 𝑏) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)))
45	44	sseq1d 3953	. . . . . 6 ⊢ (𝑏 = (𝐹 “ 𝑎) → ((𝑏 × 𝑏) ⊆ 𝑣 ↔ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣))
46	45	rspcev 3564	. . . . 5 ⊢ (((𝐹 “ 𝑎) ∈ 𝐷 ∧ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
47	29, 42, 46	syl2anc 585	. . . 4 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
48	1	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑈 ∈ (UnifOn‘𝑋))
49	2	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝐶 ∈ (CauFilu‘𝑈))
50	5	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑉 ∈ (UnifOn‘𝑌))
51	6	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝐹 ∈ (𝑈 Cnu𝑉))
52		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉)
53		nfcv 2898	. . . . . . 7 ⊢ Ⅎ𝑠⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩
54		nfcv 2898	. . . . . . 7 ⊢ Ⅎ𝑡⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩
55		nfcv 2898	. . . . . . 7 ⊢ Ⅎ𝑥⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩
56		nfcv 2898	. . . . . . 7 ⊢ Ⅎ𝑦⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩
57		simpl 482	. . . . . . . . 9 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑥 = 𝑠)
58	57	fveq2d 6844	. . . . . . . 8 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑥) = (𝐹‘𝑠))
59		simpr 484	. . . . . . . . 9 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑦 = 𝑡)
60	59	fveq2d 6844	. . . . . . . 8 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑦) = (𝐹‘𝑡))
61	58, 60	opeq12d 4824	. . . . . . 7 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ = ⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩)
62	53, 54, 55, 56, 61	cbvmpo 7461	. . . . . 6 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) = (𝑠 ∈ 𝑋, 𝑡 ∈ 𝑋 ↦ ⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩)
63	48, 50, 51, 52, 62	ucnprima 24246	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣) ∈ 𝑈)
64		cfiluexsm 24254	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈) ∧ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣) ∈ 𝑈) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣))
65	48, 49, 63, 64	syl3anc 1374	. . . 4 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣))
66	47, 65	r19.29a 3145	. . 3 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
67	66	ralrimiva 3129	. 2 ⊢ (𝜑 → ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
68		iscfilu 24252	. . 3 ⊢ (𝑉 ∈ (UnifOn‘𝑌) → (𝐷 ∈ (CauFilu‘𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)))
69	5, 68	syl 17	. 2 ⊢ (𝜑 → (𝐷 ∈ (CauFilu‘𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)))
70	13, 67, 69	mpbir2and 714	1 ⊢ (𝜑 → 𝐷 ∈ (CauFilu‘𝑉))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3051  ∃wrex 3061  Vcvv 3429   ⊆ wss 3889  ⟨cop 4573   class class class wbr 5085   ↦ cmpt 5166   × cxp 5629  ^◡ccnv 5630  ran crn 5632   “ cima 5634  Fun wfun 6492   Fn wfn 6493  ⟶wf 6494  ‘cfv 6498  (class class class)co 7367   ∈ cmpo 7369  fBascfbas 21340  UnifOncust 24165   Cn_ucucn 24239  CauFil_uccfilu 24250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-1st 7942  df-2nd 7943  df-map 8775  df-fbas 21349  df-ust 24166  df-ucn 24240  df-cfilu 24251

This theorem is referenced by:  ucnextcn  24268