Theorem fmucnd 24206

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 24203	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈)) → 𝐶 ∈ (fBas‘𝑋))
4	1, 2, 3	syl2anc 584	. . 3 ⊢ (𝜑 → 𝐶 ∈ (fBas‘𝑋))
5		fmucnd.2	. . . 4 ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌))
6		fmucnd.3	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉))
7		isucn 24192	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦)))))
8	7	simprbda 498	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) ∧ 𝐹 ∈ (𝑈 Cnu𝑉)) → 𝐹:𝑋⟶𝑌)
9	1, 5, 6, 8	syl21anc 837	. . 3 ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)
10	5	elfvexd 6858	. . 3 ⊢ (𝜑 → 𝑌 ∈ V)
11		fmucnd.5	. . . 4 ⊢ 𝐷 = ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎))
12	11	fbasrn 23799	. . 3 ⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ V) → 𝐷 ∈ (fBas‘𝑌))
13	4, 9, 10, 12	syl3anc 1373	. 2 ⊢ (𝜑 → 𝐷 ∈ (fBas‘𝑌))
14		simplr 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → 𝑎 ∈ 𝐶)
15		eqid 2731	. . . . . . . 8 ⊢ (𝐹 “ 𝑎) = (𝐹 “ 𝑎)
16		imaeq2 6004	. . . . . . . . 9 ⊢ (𝑐 = 𝑎 → (𝐹 “ 𝑐) = (𝐹 “ 𝑎))
17	16	rspceeqv 3595	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐶 ∧ (𝐹 “ 𝑎) = (𝐹 “ 𝑎)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))
18	14, 15, 17	sylancl 586	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))
19		imaexg 7843	. . . . . . . . 9 ⊢ (𝐹 ∈ (𝑈 Cnu𝑉) → (𝐹 “ 𝑎) ∈ V)
20		eqid 2731	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
21	20	elrnmpt 5897	. . . . . . . . 9 ⊢ ((𝐹 “ 𝑎) ∈ V → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)))
22	6, 19, 21	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)))
23	22	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)))
24	18, 23	mpbird 257	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → (𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)))
25		imaeq2 6004	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝐹 “ 𝑎) = (𝐹 “ 𝑐))
26	25	cbvmptv 5193	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
27	26	rneqi 5876	. . . . . . 7 ⊢ ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
28	11, 27	eqtri 2754	. . . . . 6 ⊢ 𝐷 = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))
29	24, 28	eleqtrrdi 2842	. . . . 5 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → (𝐹 “ 𝑎) ∈ 𝐷)
30	9	ffnd 6652	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn 𝑋)
31	30	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → 𝐹 Fn 𝑋)
32		fbelss 23748	. . . . . . . . 9 ⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋)
33	4, 32	sylan 580	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋)
34	33	ad4ant13 751	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → 𝑎 ⊆ 𝑋)
35		fmucndlem 24205	. . . . . . 7 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑎 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)))
36	31, 34, 35	syl2anc 584	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)))
37		eqid 2731	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
38	37	mpofun 7470	. . . . . . . 8 ⊢ Fun (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
39		funimass2 6564	. . . . . . . 8 ⊢ ((Fun (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
40	38, 39	mpan 690	. . . . . . 7 ⊢ ((𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
41	40	adantl 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
42	36, 41	eqsstrrd 3965	. . . . 5 ⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣)) → ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣)
43		id 22	. . . . . . . 8 ⊢ (𝑏 = (𝐹 “ 𝑎) → 𝑏 = (𝐹 “ 𝑎))
44	43	sqxpeqd 5646	. . . . . . 7 ⊢ (𝑏 = (𝐹 “ 𝑎) → (𝑏 × 𝑏) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)))
45	44	sseq1d 3961	. . . . . 6 ⊢ (𝑏 = (𝐹 “ 𝑎) → ((𝑏 × 𝑏) ⊆ 𝑣 ↔ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣))
46	45	rspcev 3572	. . . . 5 ⊢ (((𝐹 “ 𝑎) ∈ 𝐷 ∧ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
47	29, 42, 46	syl2anc 584	. . . 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 2894	. . . . . . 7 ⊢ Ⅎ𝑠⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩
54		nfcv 2894	. . . . . . 7 ⊢ Ⅎ𝑡⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩
55		nfcv 2894	. . . . . . 7 ⊢ Ⅎ𝑥⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩
56		nfcv 2894	. . . . . . 7 ⊢ Ⅎ𝑦⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩
57		simpl 482	. . . . . . . . 9 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑥 = 𝑠)
58	57	fveq2d 6826	. . . . . . . 8 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑥) = (𝐹‘𝑠))
59		simpr 484	. . . . . . . . 9 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑦 = 𝑡)
60	59	fveq2d 6826	. . . . . . . 8 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑦) = (𝐹‘𝑡))
61	58, 60	opeq12d 4830	. . . . . . 7 ⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩ = ⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩)
62	53, 54, 55, 56, 61	cbvmpo 7440	. . . . . 6 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) = (𝑠 ∈ 𝑋, 𝑡 ∈ 𝑋 ↦ ⟨(𝐹‘𝑠), (𝐹‘𝑡)⟩)
63	48, 50, 51, 52, 62	ucnprima 24196	. . . . 5 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣) ∈ 𝑈)
64		cfiluexsm 24204	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈) ∧ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣) ∈ 𝑈) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣))
65	48, 49, 63, 64	syl3anc 1373	. . . 4 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) “ 𝑣))
66	47, 65	r19.29a 3140	. . 3 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
67	66	ralrimiva 3124	. 2 ⊢ (𝜑 → ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
68		iscfilu 24202	. . 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 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056  Vcvv 3436   ⊆ wss 3897  ⟨cop 4579   class class class wbr 5089   ↦ cmpt 5170   × cxp 5612  ^◡ccnv 5613  ran crn 5615   “ cima 5617  Fun wfun 6475   Fn wfn 6476  ⟶wf 6477  ‘cfv 6481  (class class class)co 7346   ∈ cmpo 7348  fBascfbas 21279  UnifOncust 24115   Cn_ucucn 24189  CauFil_uccfilu 24200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-1st 7921  df-2nd 7922  df-map 8752  df-fbas 21288  df-ust 24116  df-ucn 24190  df-cfilu 24201

This theorem is referenced by:  ucnextcn  24218