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

Theorem fmucnd 22902
 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.
StepHypRef Expression
1 fmucnd.1 . . . 4 (𝜑𝑈 ∈ (UnifOn‘𝑋))
2 fmucnd.4 . . . 4 (𝜑𝐶 ∈ (CauFilu𝑈))
3 cfilufbas 22899 . . . 4 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu𝑈)) → 𝐶 ∈ (fBas‘𝑋))
41, 2, 3syl2anc 587 . . 3 (𝜑𝐶 ∈ (fBas‘𝑋))
5 fmucnd.2 . . . 4 (𝜑𝑉 ∈ (UnifOn‘𝑌))
6 fmucnd.3 . . . 4 (𝜑𝐹 ∈ (𝑈 Cnu𝑉))
7 isucn 22888 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))))
87simprbda 502 . . . 4 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) ∧ 𝐹 ∈ (𝑈 Cnu𝑉)) → 𝐹:𝑋𝑌)
91, 5, 6, 8syl21anc 836 . . 3 (𝜑𝐹:𝑋𝑌)
105elfvexd 6683 . . 3 (𝜑𝑌 ∈ V)
11 fmucnd.5 . . . 4 𝐷 = ran (𝑎𝐶 ↦ (𝐹𝑎))
1211fbasrn 22493 . . 3 ((𝐶 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌 ∈ V) → 𝐷 ∈ (fBas‘𝑌))
134, 9, 10, 12syl3anc 1368 . 2 (𝜑𝐷 ∈ (fBas‘𝑌))
14 simplr 768 . . . . . . . 8 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → 𝑎𝐶)
15 eqid 2801 . . . . . . . 8 (𝐹𝑎) = (𝐹𝑎)
16 imaeq2 5896 . . . . . . . . 9 (𝑐 = 𝑎 → (𝐹𝑐) = (𝐹𝑎))
1716rspceeqv 3589 . . . . . . . 8 ((𝑎𝐶 ∧ (𝐹𝑎) = (𝐹𝑎)) → ∃𝑐𝐶 (𝐹𝑎) = (𝐹𝑐))
1814, 15, 17sylancl 589 . . . . . . 7 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ∃𝑐𝐶 (𝐹𝑎) = (𝐹𝑐))
19 imaexg 7606 . . . . . . . . 9 (𝐹 ∈ (𝑈 Cnu𝑉) → (𝐹𝑎) ∈ V)
20 eqid 2801 . . . . . . . . . 10 (𝑐𝐶 ↦ (𝐹𝑐)) = (𝑐𝐶 ↦ (𝐹𝑐))
2120elrnmpt 5796 . . . . . . . . 9 ((𝐹𝑎) ∈ V → ((𝐹𝑎) ∈ ran (𝑐𝐶 ↦ (𝐹𝑐)) ↔ ∃𝑐𝐶 (𝐹𝑎) = (𝐹𝑐)))
226, 19, 213syl 18 . . . . . . . 8 (𝜑 → ((𝐹𝑎) ∈ ran (𝑐𝐶 ↦ (𝐹𝑐)) ↔ ∃𝑐𝐶 (𝐹𝑎) = (𝐹𝑐)))
2322ad3antrrr 729 . . . . . . 7 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ((𝐹𝑎) ∈ ran (𝑐𝐶 ↦ (𝐹𝑐)) ↔ ∃𝑐𝐶 (𝐹𝑎) = (𝐹𝑐)))
2418, 23mpbird 260 . . . . . 6 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → (𝐹𝑎) ∈ ran (𝑐𝐶 ↦ (𝐹𝑐)))
25 imaeq2 5896 . . . . . . . . 9 (𝑎 = 𝑐 → (𝐹𝑎) = (𝐹𝑐))
2625cbvmptv 5136 . . . . . . . 8 (𝑎𝐶 ↦ (𝐹𝑎)) = (𝑐𝐶 ↦ (𝐹𝑐))
2726rneqi 5775 . . . . . . 7 ran (𝑎𝐶 ↦ (𝐹𝑎)) = ran (𝑐𝐶 ↦ (𝐹𝑐))
2811, 27eqtri 2824 . . . . . 6 𝐷 = ran (𝑐𝐶 ↦ (𝐹𝑐))
2924, 28eleqtrrdi 2904 . . . . 5 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → (𝐹𝑎) ∈ 𝐷)
309ffnd 6492 . . . . . . . 8 (𝜑𝐹 Fn 𝑋)
3130ad3antrrr 729 . . . . . . 7 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → 𝐹 Fn 𝑋)
32 fbelss 22442 . . . . . . . . 9 ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑎𝐶) → 𝑎𝑋)
334, 32sylan 583 . . . . . . . 8 ((𝜑𝑎𝐶) → 𝑎𝑋)
3433ad4ant13 750 . . . . . . 7 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → 𝑎𝑋)
35 fmucndlem 22901 . . . . . . 7 ((𝐹 Fn 𝑋𝑎𝑋) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹𝑎) × (𝐹𝑎)))
3631, 34, 35syl2anc 587 . . . . . 6 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹𝑎) × (𝐹𝑎)))
37 eqid 2801 . . . . . . . . 9 (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) = (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩)
3837mpofun 7259 . . . . . . . 8 Fun (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩)
39 funimass2 6411 . . . . . . . 8 ((Fun (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
4038, 39mpan 689 . . . . . . 7 ((𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
4140adantl 485 . . . . . 6 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
4236, 41eqsstrrd 3957 . . . . 5 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ((𝐹𝑎) × (𝐹𝑎)) ⊆ 𝑣)
43 id 22 . . . . . . . 8 (𝑏 = (𝐹𝑎) → 𝑏 = (𝐹𝑎))
4443sqxpeqd 5555 . . . . . . 7 (𝑏 = (𝐹𝑎) → (𝑏 × 𝑏) = ((𝐹𝑎) × (𝐹𝑎)))
4544sseq1d 3949 . . . . . 6 (𝑏 = (𝐹𝑎) → ((𝑏 × 𝑏) ⊆ 𝑣 ↔ ((𝐹𝑎) × (𝐹𝑎)) ⊆ 𝑣))
4645rspcev 3574 . . . . 5 (((𝐹𝑎) ∈ 𝐷 ∧ ((𝐹𝑎) × (𝐹𝑎)) ⊆ 𝑣) → ∃𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
4729, 42, 46syl2anc 587 . . . 4 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ∃𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
481adantr 484 . . . . 5 ((𝜑𝑣𝑉) → 𝑈 ∈ (UnifOn‘𝑋))
492adantr 484 . . . . 5 ((𝜑𝑣𝑉) → 𝐶 ∈ (CauFilu𝑈))
505adantr 484 . . . . . 6 ((𝜑𝑣𝑉) → 𝑉 ∈ (UnifOn‘𝑌))
516adantr 484 . . . . . 6 ((𝜑𝑣𝑉) → 𝐹 ∈ (𝑈 Cnu𝑉))
52 simpr 488 . . . . . 6 ((𝜑𝑣𝑉) → 𝑣𝑉)
53 nfcv 2958 . . . . . . 7 𝑠⟨(𝐹𝑥), (𝐹𝑦)⟩
54 nfcv 2958 . . . . . . 7 𝑡⟨(𝐹𝑥), (𝐹𝑦)⟩
55 nfcv 2958 . . . . . . 7 𝑥⟨(𝐹𝑠), (𝐹𝑡)⟩
56 nfcv 2958 . . . . . . 7 𝑦⟨(𝐹𝑠), (𝐹𝑡)⟩
57 simpl 486 . . . . . . . . 9 ((𝑥 = 𝑠𝑦 = 𝑡) → 𝑥 = 𝑠)
5857fveq2d 6653 . . . . . . . 8 ((𝑥 = 𝑠𝑦 = 𝑡) → (𝐹𝑥) = (𝐹𝑠))
59 simpr 488 . . . . . . . . 9 ((𝑥 = 𝑠𝑦 = 𝑡) → 𝑦 = 𝑡)
6059fveq2d 6653 . . . . . . . 8 ((𝑥 = 𝑠𝑦 = 𝑡) → (𝐹𝑦) = (𝐹𝑡))
6158, 60opeq12d 4776 . . . . . . 7 ((𝑥 = 𝑠𝑦 = 𝑡) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ = ⟨(𝐹𝑠), (𝐹𝑡)⟩)
6253, 54, 55, 56, 61cbvmpo 7231 . . . . . 6 (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) = (𝑠𝑋, 𝑡𝑋 ↦ ⟨(𝐹𝑠), (𝐹𝑡)⟩)
6348, 50, 51, 52, 62ucnprima 22892 . . . . 5 ((𝜑𝑣𝑉) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣) ∈ 𝑈)
64 cfiluexsm 22900 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu𝑈) ∧ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣) ∈ 𝑈) → ∃𝑎𝐶 (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣))
6548, 49, 63, 64syl3anc 1368 . . . 4 ((𝜑𝑣𝑉) → ∃𝑎𝐶 (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣))
6647, 65r19.29a 3251 . . 3 ((𝜑𝑣𝑉) → ∃𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
6766ralrimiva 3152 . 2 (𝜑 → ∀𝑣𝑉𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
68 iscfilu 22898 . . 3 (𝑉 ∈ (UnifOn‘𝑌) → (𝐷 ∈ (CauFilu𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣𝑉𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)))
695, 68syl 17 . 2 (𝜑 → (𝐷 ∈ (CauFilu𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣𝑉𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)))
7013, 67, 69mpbir2and 712 1 (𝜑𝐷 ∈ (CauFilu𝑉))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2112  ∀wral 3109  ∃wrex 3110  Vcvv 3444   ⊆ wss 3884  ⟨cop 4534   class class class wbr 5033   ↦ cmpt 5113   × cxp 5521  ◡ccnv 5522  ran crn 5524   “ cima 5526  Fun wfun 6322   Fn wfn 6323  ⟶wf 6324  ‘cfv 6328  (class class class)co 7139   ∈ cmpo 7141  fBascfbas 20083  UnifOncust 22809   Cnucucn 22885  CauFiluccfilu 22896 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-1st 7675  df-2nd 7676  df-map 8395  df-fbas 20092  df-ust 22810  df-ucn 22886  df-cfilu 22897 This theorem is referenced by:  ucnextcn  22914
 Copyright terms: Public domain W3C validator