Theorem fmucnd 24322

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 24319	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈)) → 𝐶 ∈ (fBas‘𝑋))
4	1, 2, 3	syl2anc 583	. . 3 ⊢ (𝜑 → 𝐶 ∈ (fBas‘𝑋))
5		fmucnd.2	. . . 4 ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))
6		fmucnd.3	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))
7		isucn 24308	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)))))
8	7	simprbda 498	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) ∧ 𝐹 ∈ (𝑈 Cnu𝑉)) → 𝐹:𝑋⟶𝑌)
9	1, 5, 6, 8	syl21anc 837	. . 3 ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)
10	5	elfvexd 6959	. . 3 ⊢ (𝜑 → 𝑌 ∈ V)
11		fmucnd.5	. . . 4 ⊢ 𝐷 = ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎))
12	11	fbasrn 23913	. . 3 ⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ V) → 𝐷 ∈ (fBas‘𝑌))
13	4, 9, 10, 12	syl3anc 1371	. 2 ⊢ (𝜑 → 𝐷 ∈ (fBas‘𝑌))
14		simplr 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → 𝑎 ∈ 𝐶)
15		eqid 2740	. . . . . . . 8 ⊢ (𝐹 “ 𝑎) = (𝐹 “ 𝑎)
16		imaeq2 6085	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → (𝐹 “ 𝑐) = (𝐹 “ 𝑎))
17	16	rspceeqv 3658	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐶 ∧ (𝐹 “ 𝑎) = (𝐹 “ 𝑎)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))
18	14, 15, 17	sylancl 585	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))
19		imaexg 7953	. . . . . . . . 9 ⊢ (𝐹 ∈ (𝑈 Cnu𝑉) → (𝐹 “ 𝑎) ∈ V)
20		eqid 2740	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
21	20	elrnmpt 5981	. . . . . . . . 9 ⊢ ((𝐹 “ 𝑎) ∈ V → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)))
22	6, 19, 21	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)))
23	22	ad3antrrr 729	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)))
24	18, 23	mpbird 257	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → (𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)))
25		imaeq2 6085	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝐹 “ 𝑎) = (𝐹 “ 𝑐))
26	25	cbvmptv 5279	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
27	26	rneqi 5962	. . . . . . 7 ⊢ ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
28	11, 27	eqtri 2768	. . . . . 6 ⊢ 𝐷 = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
29	24, 28	eleqtrrdi 2855	. . . . 5 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → (𝐹 “ 𝑎) ∈ 𝐷)
30	9	ffnd 6748	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn 𝑋)
31	30	ad3antrrr 729	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → 𝐹 Fn 𝑋)
32		fbelss 23862	. . . . . . . . 9 ⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋)
33	4, 32	sylan 579	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋)
34	33	ad4ant13 750	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → 𝑎 ⊆ 𝑋)
35		fmucndlem 24321	. . . . . . 7 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑎 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)))
36	31, 34, 35	syl2anc 583	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)))
37		eqid 2740	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
38	37	mpofun 7574	. . . . . . . 8 ⊢ Fun (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
39		funimass2 6661	. . . . . . . 8 ⊢ ((Fun (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
40	38, 39	mpan 689	. . . . . . 7 ⊢ ((𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
41	40	adantl 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
42	36, 41	eqsstrrd 4048	. . . . 5 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣)
43		id 22	. . . . . . . 8 ⊢ (𝑏 = (𝐹 “ 𝑎) → 𝑏 = (𝐹 “ 𝑎))
44	43	sqxpeqd 5732	. . . . . . 7 ⊢ (𝑏 = (𝐹 “ 𝑎) → (𝑏 × 𝑏) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)))
45	44	sseq1d 4040	. . . . . 6 ⊢ (𝑏 = (𝐹 “ 𝑎) → ((𝑏 × 𝑏) ⊆ 𝑣 ↔ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣))
46	45	rspcev 3635	. . . . 5 ⊢ (((𝐹 “ 𝑎) ∈ 𝐷 ∧ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
47	29, 42, 46	syl2anc 583	. . . 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 2908	. . . . . . 7 ⊢ Ⅎ𝑠⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩
54		nfcv 2908	. . . . . . 7 ⊢ Ⅎ𝑡⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩
55		nfcv 2908	. . . . . . 7 ⊢ Ⅎ𝑥⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩
56		nfcv 2908	. . . . . . 7 ⊢ Ⅎ𝑦⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩
57		simpl 482	. . . . . . . . 9 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑥 = 𝑠)
58	57	fveq2d 6924	. . . . . . . 8 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑥) = (𝐹‘𝑠))
59		simpr 484	. . . . . . . . 9 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑦 = 𝑡)
60	59	fveq2d 6924	. . . . . . . 8 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑦) = (𝐹‘𝑡))
61	58, 60	opeq12d 4905	. . . . . . 7 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ = ⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩)
62	53, 54, 55, 56, 61	cbvmpo 7544	. . . . . 6 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) = (𝑠 ∈ 𝑋, 𝑡 ∈ 𝑋 ↦ ⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩)
63	48, 50, 51, 52, 62	ucnprima 24312	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣) ∈ 𝑈)
64		cfiluexsm 24320	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈) ∧ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣) ∈ 𝑈) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣))
65	48, 49, 63, 64	syl3anc 1371	. . . 4 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣))
66	47, 65	r19.29a 3168	. . 3 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
67	66	ralrimiva 3152	. 2 ⊢ (𝜑 → ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
68		iscfilu 24318	. . 3 ⊢ (𝑉 ∈ (UnifOn‘𝑌) → (𝐷 ∈ (CauFilu‘𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)))
69	5, 68	syl 17	. 2 ⊢ (𝜑 → (𝐷 ∈ (CauFilu‘𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)))
70	13, 67, 69	mpbir2and 712	1 ⊢ (𝜑 → 𝐷 ∈ (CauFilu‘𝑉))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ∃wrex 3076  Vcvv 3488   ⊆ wss 3976  ⟨cop 4654   class class class wbr 5166   ↦ cmpt 5249   × cxp 5698  ^◡ccnv 5699  ran crn 5701   “ cima 5703  Fun wfun 6567   Fn wfn 6568  ⟶wf 6569  ‘cfv 6573  (class class class)co 7448   ∈ cmpo 7450  fBascfbas 21375  UnifOncust 24229   Cn_ucucn 24305  CauFil_uccfilu 24316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-map 8886  df-fbas 21384  df-ust 24230  df-ucn 24306  df-cfilu 24317

This theorem is referenced by:  ucnextcn  24334