ucnval - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ucnval		Structured version Visualization version GIF version

Theorem ucnval 24595

Description: The set of all uniformly continuous function from uniform space 𝑈 to uniform space 𝑉. (Contributed by Thierry Arnoux, 16-Nov-2017.)

**Assertion**
Ref	Expression
ucnval	⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝑈 Cn_u𝑉) = {𝑓 ∈ (𝑌 ↑_m 𝑋) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})

Distinct variable groups: 𝑓,𝑟,𝑠,𝑥,𝑦,𝑈 𝑓,𝑉,𝑟,𝑠,𝑥 𝑓,𝑋,𝑟,𝑠,𝑥,𝑦 𝑓,𝑌,𝑟,𝑠,𝑥 Allowed substitution hints: 𝑉(𝑦) 𝑌(𝑦)

Proof of Theorem ucnval Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfvunirn 6915	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ∈ ∪ ran UnifOn)
2	1	adantr 486	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → 𝑈 ∈ ∪ ran UnifOn)
3		elfvunirn 6915	. . . 4 ⊢ (𝑉 ∈ (UnifOn‘𝑌) → 𝑉 ∈ ∪ ran UnifOn)
4	3	adantl 487	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → 𝑉 ∈ ∪ ran UnifOn)
5		ovex 7453	. . . . 5 ⊢ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∈ V
6	5	rabex 5299	. . . 4 ⊢ {𝑓 ∈ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))} ∈ V
7	6	a1i 11	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → {𝑓 ∈ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))} ∈ V)
8		simpr 490	. . . . . . . 8 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑣 = 𝑉)
9	8	unieqd 4879	. . . . . . 7 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ∪ 𝑣 = ∪ 𝑉)
10	9	dmeqd 5886	. . . . . 6 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → dom ∪ 𝑣 = dom ∪ 𝑉)
11		simpl 488	. . . . . . . 8 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑢 = 𝑈)
12	11	unieqd 4879	. . . . . . 7 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ∪ 𝑢 = ∪ 𝑈)
13	12	dmeqd 5886	. . . . . 6 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → dom ∪ 𝑢 = dom ∪ 𝑈)
14	10, 13	oveq12d 7438	. . . . 5 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (dom ∪ 𝑣 ↑_m dom ∪ 𝑢) = (dom ∪ 𝑉 ↑_m dom ∪ 𝑈))
15	13	raleqdv 3319	. . . . . . . 8 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
16	13, 15	raleqbidv 3334	. . . . . . 7 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
17	11, 16	rexeqbidv 3335	. . . . . 6 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
18	8, 17	raleqbidv 3334	. . . . 5 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (∀𝑠 ∈ 𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
19	14, 18	rabeqbidv 3429	. . . 4 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → {𝑓 ∈ (dom ∪ 𝑣 ↑_m dom ∪ 𝑢) ∣ ∀𝑠 ∈ 𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))} = {𝑓 ∈ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
20		df-ucn 24594	. . . 4 ⊢ Cn_u = (𝑢 ∈ ∪ ran UnifOn, 𝑣 ∈ ∪ ran UnifOn ↦ {𝑓 ∈ (dom ∪ 𝑣 ↑_m dom ∪ 𝑢) ∣ ∀𝑠 ∈ 𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
21	19, 20	ovmpoga 7574	. . 3 ⊢ ((𝑈 ∈ ∪ ran UnifOn ∧ 𝑉 ∈ ∪ ran UnifOn ∧ {𝑓 ∈ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))} ∈ V) → (𝑈 Cn_u𝑉) = {𝑓 ∈ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
22	2, 4, 7, 21	syl3anc 1398	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝑈 Cn_u𝑉) = {𝑓 ∈ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
23		ustbas2 24544	. . . 4 ⊢ (𝑉 ∈ (UnifOn‘𝑌) → 𝑌 = dom ∪ 𝑉)
24		ustbas2 24544	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = dom ∪ 𝑈)
25	23, 24	oveqan12rd 7440	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝑌 ↑_m 𝑋) = (dom ∪ 𝑉 ↑_m dom ∪ 𝑈))
26	24	adantr 486	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → 𝑋 = dom ∪ 𝑈)
27	26	raleqdv 3319	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
28	26, 27	raleqbidv 3334	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
29	28	rexbidv 3186	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
30	29	ralbidv 3185	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
31	25, 30	rabeqbidv 3429	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → {𝑓 ∈ (𝑌 ↑_m 𝑋) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))} = {𝑓 ∈ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
32	22, 31	eqtr4d 2798	1 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝑈 Cn_u𝑉) = {𝑓 ∈ (𝑌 ↑_m 𝑋) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ∀wral 3076 ∃wrex 3086 {crab 3412 Vcvv 3450 ∪ cuni 4866 class class class wbr 5102 dom cdm 5650 ran crn 5651 ‘cfv 6538 (class class class)co 7420 ↑_m cmap 8847 UnifOncust 24519 Cn_ucucn 24593

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-sbc 3739 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-iota 6494 df-fun 6540 df-fv 6546 df-ov 7423 df-oprab 7424 df-mpo 7425 df-ust 24520 df-ucn 24594

This theorem is used by: isucn 24596

W3C validator