Theorem fmucnd 24291

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 24288	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈)) → 𝐶 ∈ (fBas‘𝑋))
4	1, 2, 3	syl2anc 582	. . 3 ⊢ (𝜑 → 𝐶 ∈ (fBas‘𝑋))
5		fmucnd.2	. . . 4 ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))
6		fmucnd.3	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))
7		isucn 24277	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)))))
8	7	simprbda 497	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) ∧ 𝐹 ∈ (𝑈 Cnu𝑉)) → 𝐹:𝑋⟶𝑌)
9	1, 5, 6, 8	syl21anc 836	. . 3 ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)
10	5	elfvexd 6942	. . 3 ⊢ (𝜑 → 𝑌 ∈ V)
11		fmucnd.5	. . . 4 ⊢ 𝐷 = ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎))
12	11	fbasrn 23882	. . 3 ⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ V) → 𝐷 ∈ (fBas‘𝑌))
13	4, 9, 10, 12	syl3anc 1368	. 2 ⊢ (𝜑 → 𝐷 ∈ (fBas‘𝑌))
14		simplr 767	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → 𝑎 ∈ 𝐶)
15		eqid 2726	. . . . . . . 8 ⊢ (𝐹 “ 𝑎) = (𝐹 “ 𝑎)
16		imaeq2 6067	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → (𝐹 “ 𝑐) = (𝐹 “ 𝑎))
17	16	rspceeqv 3630	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐶 ∧ (𝐹 “ 𝑎) = (𝐹 “ 𝑎)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))
18	14, 15, 17	sylancl 584	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))
19		imaexg 7928	. . . . . . . . 9 ⊢ (𝐹 ∈ (𝑈 Cnu𝑉) → (𝐹 “ 𝑎) ∈ V)
20		eqid 2726	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
21	20	elrnmpt 5964	. . . . . . . . 9 ⊢ ((𝐹 “ 𝑎) ∈ V → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)))
22	6, 19, 21	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)))
23	22	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)))
24	18, 23	mpbird 256	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → (𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)))
25		imaeq2 6067	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝐹 “ 𝑎) = (𝐹 “ 𝑐))
26	25	cbvmptv 5268	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
27	26	rneqi 5945	. . . . . . 7 ⊢ ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
28	11, 27	eqtri 2754	. . . . . 6 ⊢ 𝐷 = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
29	24, 28	eleqtrrdi 2837	. . . . 5 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → (𝐹 “ 𝑎) ∈ 𝐷)
30	9	ffnd 6731	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn 𝑋)
31	30	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → 𝐹 Fn 𝑋)
32		fbelss 23831	. . . . . . . . 9 ⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋)
33	4, 32	sylan 578	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋)
34	33	ad4ant13 749	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → 𝑎 ⊆ 𝑋)
35		fmucndlem 24290	. . . . . . 7 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑎 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)))
36	31, 34, 35	syl2anc 582	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)))
37		eqid 2726	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
38	37	mpofun 7551	. . . . . . . 8 ⊢ Fun (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
39		funimass2 6644	. . . . . . . 8 ⊢ ((Fun (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
40	38, 39	mpan 688	. . . . . . 7 ⊢ ((𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
41	40	adantl 480	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
42	36, 41	eqsstrrd 4019	. . . . 5 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣)
43		id 22	. . . . . . . 8 ⊢ (𝑏 = (𝐹 “ 𝑎) → 𝑏 = (𝐹 “ 𝑎))
44	43	sqxpeqd 5716	. . . . . . 7 ⊢ (𝑏 = (𝐹 “ 𝑎) → (𝑏 × 𝑏) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)))
45	44	sseq1d 4011	. . . . . 6 ⊢ (𝑏 = (𝐹 “ 𝑎) → ((𝑏 × 𝑏) ⊆ 𝑣 ↔ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣))
46	45	rspcev 3608	. . . . 5 ⊢ (((𝐹 “ 𝑎) ∈ 𝐷 ∧ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
47	29, 42, 46	syl2anc 582	. . . 4 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
48	1	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑈 ∈ (UnifOn‘𝑋))
49	2	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝐶 ∈ (CauFilu‘𝑈))
50	5	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑉 ∈ (UnifOn‘𝑌))
51	6	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝐹 ∈ (𝑈 Cnu𝑉))
52		simpr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉)
53		nfcv 2892	. . . . . . 7 ⊢ Ⅎ𝑠⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩
54		nfcv 2892	. . . . . . 7 ⊢ Ⅎ𝑡⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩
55		nfcv 2892	. . . . . . 7 ⊢ Ⅎ𝑥⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩
56		nfcv 2892	. . . . . . 7 ⊢ Ⅎ𝑦⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩
57		simpl 481	. . . . . . . . 9 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑥 = 𝑠)
58	57	fveq2d 6907	. . . . . . . 8 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑥) = (𝐹‘𝑠))
59		simpr 483	. . . . . . . . 9 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑦 = 𝑡)
60	59	fveq2d 6907	. . . . . . . 8 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑦) = (𝐹‘𝑡))
61	58, 60	opeq12d 4889	. . . . . . 7 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ = ⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩)
62	53, 54, 55, 56, 61	cbvmpo 7521	. . . . . 6 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) = (𝑠 ∈ 𝑋, 𝑡 ∈ 𝑋 ↦ ⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩)
63	48, 50, 51, 52, 62	ucnprima 24281	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣) ∈ 𝑈)
64		cfiluexsm 24289	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈) ∧ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣) ∈ 𝑈) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣))
65	48, 49, 63, 64	syl3anc 1368	. . . 4 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣))
66	47, 65	r19.29a 3152	. . 3 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
67	66	ralrimiva 3136	. 2 ⊢ (𝜑 → ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
68		iscfilu 24287	. . 3 ⊢ (𝑉 ∈ (UnifOn‘𝑌) → (𝐷 ∈ (CauFilu‘𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)))
69	5, 68	syl 17	. 2 ⊢ (𝜑 → (𝐷 ∈ (CauFilu‘𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)))
70	13, 67, 69	mpbir2and 711	1 ⊢ (𝜑 → 𝐷 ∈ (CauFilu‘𝑉))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1534   ∈ wcel 2099  ∀wral 3051  ∃wrex 3060  Vcvv 3462   ⊆ wss 3947  ⟨cop 4639   class class class wbr 5155   ↦ cmpt 5238   × cxp 5682  ^◡ccnv 5683  ran crn 5685   “ cima 5687  Fun wfun 6550   Fn wfn 6551  ⟶wf 6552  ‘cfv 6556  (class class class)co 7426   ∈ cmpo 7428  fBascfbas 21333  UnifOncust 24198   Cn_ucucn 24274  CauFil_uccfilu 24285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5292  ax-sep 5306  ax-nul 5313  ax-pow 5371  ax-pr 5435  ax-un 7748

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4916  df-iun 5005  df-br 5156  df-opab 5218  df-mpt 5239  df-id 5582  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-fv 6564  df-ov 7429  df-oprab 7430  df-mpo 7431  df-1st 8005  df-2nd 8006  df-map 8859  df-fbas 21342  df-ust 24199  df-ucn 24275  df-cfilu 24286

This theorem is referenced by:  ucnextcn  24303