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 22888

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		elrnust 22835	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ∈ ∪ ran UnifOn)
2	1	adantr 483	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → 𝑈 ∈ ∪ ran UnifOn)
3		elrnust 22835	. . . 4 ⊢ (𝑉 ∈ (UnifOn‘𝑌) → 𝑉 ∈ ∪ ran UnifOn)
4	3	adantl 484	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → 𝑉 ∈ ∪ ran UnifOn)
5		ovex 7191	. . . . 5 ⊢ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∈ V
6	5	rabex 5237	. . . 4 ⊢ {𝑓 ∈ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))} ∈ V
7	6	a1i 11	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → {𝑓 ∈ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))} ∈ V)
8		simpr 487	. . . . . . . 8 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑣 = 𝑉)
9	8	unieqd 4854	. . . . . . 7 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ∪ 𝑣 = ∪ 𝑉)
10	9	dmeqd 5776	. . . . . 6 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → dom ∪ 𝑣 = dom ∪ 𝑉)
11		simpl 485	. . . . . . . 8 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑢 = 𝑈)
12	11	unieqd 4854	. . . . . . 7 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ∪ 𝑢 = ∪ 𝑈)
13	12	dmeqd 5776	. . . . . 6 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → dom ∪ 𝑢 = dom ∪ 𝑈)
14	10, 13	oveq12d 7176	. . . . 5 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (dom ∪ 𝑣 ↑_m dom ∪ 𝑢) = (dom ∪ 𝑉 ↑_m dom ∪ 𝑈))
15	13	raleqdv 3417	. . . . . . . 8 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
16	13, 15	raleqbidv 3403	. . . . . . 7 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
17	11, 16	rexeqbidv 3404	. . . . . 6 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
18	8, 17	raleqbidv 3403	. . . . 5 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (∀𝑠 ∈ 𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
19	14, 18	rabeqbidv 3487	. . . 4 ⊢ ((𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → {𝑓 ∈ (dom ∪ 𝑣 ↑_m dom ∪ 𝑢) ∣ ∀𝑠 ∈ 𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))} = {𝑓 ∈ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
20		df-ucn 22887	. . . 4 ⊢ Cn_u = (𝑢 ∈ ∪ ran UnifOn, 𝑣 ∈ ∪ ran UnifOn ↦ {𝑓 ∈ (dom ∪ 𝑣 ↑_m dom ∪ 𝑢) ∣ ∀𝑠 ∈ 𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
21	19, 20	ovmpoga 7306	. . 3 ⊢ ((𝑈 ∈ ∪ ran UnifOn ∧ 𝑉 ∈ ∪ ran UnifOn ∧ {𝑓 ∈ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))} ∈ V) → (𝑈 Cn_u𝑉) = {𝑓 ∈ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
22	2, 4, 7, 21	syl3anc 1367	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝑈 Cn_u𝑉) = {𝑓 ∈ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
23		ustbas2 22836	. . . 4 ⊢ (𝑉 ∈ (UnifOn‘𝑌) → 𝑌 = dom ∪ 𝑉)
24		ustbas2 22836	. . . 4 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = dom ∪ 𝑈)
25	23, 24	oveqan12rd 7178	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝑌 ↑_m 𝑋) = (dom ∪ 𝑉 ↑_m dom ∪ 𝑈))
26	24	adantr 483	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → 𝑋 = dom ∪ 𝑈)
27	26	raleqdv 3417	. . . . . 6 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
28	26, 27	raleqbidv 3403	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
29	28	rexbidv 3299	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
30	29	ralbidv 3199	. . 3 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦)) ↔ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))))
31	25, 30	rabeqbidv 3487	. 2 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → {𝑓 ∈ (𝑌 ↑_m 𝑋) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))} = {𝑓 ∈ (dom ∪ 𝑉 ↑_m dom ∪ 𝑈) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ dom ∪ 𝑈∀𝑦 ∈ dom ∪ 𝑈(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})
32	22, 31	eqtr4d 2861	1 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝑈 Cn_u𝑉) = {𝑓 ∈ (𝑌 ↑_m 𝑋) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ∀wral 3140 ∃wrex 3141 {crab 3144 Vcvv 3496 ∪ cuni 4840 class class class wbr 5068 dom cdm 5557 ran crn 5558 ‘cfv 6357 (class class class)co 7158 ↑_m cmap 8408 UnifOncust 22810 Cn_ucucn 22886

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 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-sbc 3775 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4841 df-br 5069 df-opab 5131 df-mpt 5149 df-id 5462 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-iota 6316 df-fun 6359 df-fn 6360 df-fv 6365 df-ov 7161 df-oprab 7162 df-mpo 7163 df-ust 22811 df-ucn 22887

This theorem is referenced by: isucn 22889

W3C validator