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

Theorem fmucnd 21906
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 21903 . . . 4 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu𝑈)) → 𝐶 ∈ (fBas‘𝑋))
41, 2, 3syl2anc 691 . . 3 (𝜑𝐶 ∈ (fBas‘𝑋))
5 fmucnd.2 . . . 4 (𝜑𝑉 ∈ (UnifOn‘𝑌))
6 fmucnd.3 . . . 4 (𝜑𝐹 ∈ (𝑈 Cnu𝑉))
7 isucn 21892 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))))
87simprbda 651 . . . 4 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) ∧ 𝐹 ∈ (𝑈 Cnu𝑉)) → 𝐹:𝑋𝑌)
91, 5, 6, 8syl21anc 1317 . . 3 (𝜑𝐹:𝑋𝑌)
105elfvexd 6132 . . 3 (𝜑𝑌 ∈ V)
11 fmucnd.5 . . . 4 𝐷 = ran (𝑎𝐶 ↦ (𝐹𝑎))
1211fbasrn 21498 . . 3 ((𝐶 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌 ∈ V) → 𝐷 ∈ (fBas‘𝑌))
134, 9, 10, 12syl3anc 1318 . 2 (𝜑𝐷 ∈ (fBas‘𝑌))
14 simplr 788 . . . . . . . 8 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → 𝑎𝐶)
15 eqid 2610 . . . . . . . 8 (𝐹𝑎) = (𝐹𝑎)
16 imaeq2 5381 . . . . . . . . . 10 (𝑐 = 𝑎 → (𝐹𝑐) = (𝐹𝑎))
1716eqeq2d 2620 . . . . . . . . 9 (𝑐 = 𝑎 → ((𝐹𝑎) = (𝐹𝑐) ↔ (𝐹𝑎) = (𝐹𝑎)))
1817rspcev 3282 . . . . . . . 8 ((𝑎𝐶 ∧ (𝐹𝑎) = (𝐹𝑎)) → ∃𝑐𝐶 (𝐹𝑎) = (𝐹𝑐))
1914, 15, 18sylancl 693 . . . . . . 7 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ∃𝑐𝐶 (𝐹𝑎) = (𝐹𝑐))
20 imaexg 6995 . . . . . . . . 9 (𝐹 ∈ (𝑈 Cnu𝑉) → (𝐹𝑎) ∈ V)
21 eqid 2610 . . . . . . . . . 10 (𝑐𝐶 ↦ (𝐹𝑐)) = (𝑐𝐶 ↦ (𝐹𝑐))
2221elrnmpt 5293 . . . . . . . . 9 ((𝐹𝑎) ∈ V → ((𝐹𝑎) ∈ ran (𝑐𝐶 ↦ (𝐹𝑐)) ↔ ∃𝑐𝐶 (𝐹𝑎) = (𝐹𝑐)))
236, 20, 223syl 18 . . . . . . . 8 (𝜑 → ((𝐹𝑎) ∈ ran (𝑐𝐶 ↦ (𝐹𝑐)) ↔ ∃𝑐𝐶 (𝐹𝑎) = (𝐹𝑐)))
2423ad3antrrr 762 . . . . . . 7 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ((𝐹𝑎) ∈ ran (𝑐𝐶 ↦ (𝐹𝑐)) ↔ ∃𝑐𝐶 (𝐹𝑎) = (𝐹𝑐)))
2519, 24mpbird 246 . . . . . 6 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → (𝐹𝑎) ∈ ran (𝑐𝐶 ↦ (𝐹𝑐)))
26 imaeq2 5381 . . . . . . . . 9 (𝑎 = 𝑐 → (𝐹𝑎) = (𝐹𝑐))
2726cbvmptv 4678 . . . . . . . 8 (𝑎𝐶 ↦ (𝐹𝑎)) = (𝑐𝐶 ↦ (𝐹𝑐))
2827rneqi 5273 . . . . . . 7 ran (𝑎𝐶 ↦ (𝐹𝑎)) = ran (𝑐𝐶 ↦ (𝐹𝑐))
2911, 28eqtri 2632 . . . . . 6 𝐷 = ran (𝑐𝐶 ↦ (𝐹𝑐))
3025, 29syl6eleqr 2699 . . . . 5 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → (𝐹𝑎) ∈ 𝐷)
31 ffn 5958 . . . . . . . . 9 (𝐹:𝑋𝑌𝐹 Fn 𝑋)
329, 31syl 17 . . . . . . . 8 (𝜑𝐹 Fn 𝑋)
3332ad3antrrr 762 . . . . . . 7 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → 𝐹 Fn 𝑋)
34 simplll 794 . . . . . . . 8 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → 𝜑)
35 fbelss 21447 . . . . . . . . 9 ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑎𝐶) → 𝑎𝑋)
364, 35sylan 487 . . . . . . . 8 ((𝜑𝑎𝐶) → 𝑎𝑋)
3734, 14, 36syl2anc 691 . . . . . . 7 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → 𝑎𝑋)
38 fmucndlem 21905 . . . . . . 7 ((𝐹 Fn 𝑋𝑎𝑋) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹𝑎) × (𝐹𝑎)))
3933, 37, 38syl2anc 691 . . . . . 6 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹𝑎) × (𝐹𝑎)))
40 eqid 2610 . . . . . . . . 9 (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) = (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩)
4140mpt2fun 6660 . . . . . . . 8 Fun (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩)
42 funimass2 5886 . . . . . . . 8 ((Fun (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
4341, 42mpan 702 . . . . . . 7 ((𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
4443adantl 481 . . . . . 6 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
4539, 44eqsstr3d 3603 . . . . 5 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ((𝐹𝑎) × (𝐹𝑎)) ⊆ 𝑣)
46 id 22 . . . . . . . 8 (𝑏 = (𝐹𝑎) → 𝑏 = (𝐹𝑎))
4746sqxpeqd 5065 . . . . . . 7 (𝑏 = (𝐹𝑎) → (𝑏 × 𝑏) = ((𝐹𝑎) × (𝐹𝑎)))
4847sseq1d 3595 . . . . . 6 (𝑏 = (𝐹𝑎) → ((𝑏 × 𝑏) ⊆ 𝑣 ↔ ((𝐹𝑎) × (𝐹𝑎)) ⊆ 𝑣))
4948rspcev 3282 . . . . 5 (((𝐹𝑎) ∈ 𝐷 ∧ ((𝐹𝑎) × (𝐹𝑎)) ⊆ 𝑣) → ∃𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
5030, 45, 49syl2anc 691 . . . 4 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ∃𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
511adantr 480 . . . . 5 ((𝜑𝑣𝑉) → 𝑈 ∈ (UnifOn‘𝑋))
522adantr 480 . . . . 5 ((𝜑𝑣𝑉) → 𝐶 ∈ (CauFilu𝑈))
535adantr 480 . . . . . 6 ((𝜑𝑣𝑉) → 𝑉 ∈ (UnifOn‘𝑌))
546adantr 480 . . . . . 6 ((𝜑𝑣𝑉) → 𝐹 ∈ (𝑈 Cnu𝑉))
55 simpr 476 . . . . . 6 ((𝜑𝑣𝑉) → 𝑣𝑉)
56 nfcv 2751 . . . . . . 7 𝑠⟨(𝐹𝑥), (𝐹𝑦)⟩
57 nfcv 2751 . . . . . . 7 𝑡⟨(𝐹𝑥), (𝐹𝑦)⟩
58 nfcv 2751 . . . . . . 7 𝑥⟨(𝐹𝑠), (𝐹𝑡)⟩
59 nfcv 2751 . . . . . . 7 𝑦⟨(𝐹𝑠), (𝐹𝑡)⟩
60 simpl 472 . . . . . . . . 9 ((𝑥 = 𝑠𝑦 = 𝑡) → 𝑥 = 𝑠)
6160fveq2d 6107 . . . . . . . 8 ((𝑥 = 𝑠𝑦 = 𝑡) → (𝐹𝑥) = (𝐹𝑠))
62 simpr 476 . . . . . . . . 9 ((𝑥 = 𝑠𝑦 = 𝑡) → 𝑦 = 𝑡)
6362fveq2d 6107 . . . . . . . 8 ((𝑥 = 𝑠𝑦 = 𝑡) → (𝐹𝑦) = (𝐹𝑡))
6461, 63opeq12d 4348 . . . . . . 7 ((𝑥 = 𝑠𝑦 = 𝑡) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ = ⟨(𝐹𝑠), (𝐹𝑡)⟩)
6556, 57, 58, 59, 64cbvmpt2 6632 . . . . . 6 (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) = (𝑠𝑋, 𝑡𝑋 ↦ ⟨(𝐹𝑠), (𝐹𝑡)⟩)
6651, 53, 54, 55, 65ucnprima 21896 . . . . 5 ((𝜑𝑣𝑉) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣) ∈ 𝑈)
67 cfiluexsm 21904 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu𝑈) ∧ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣) ∈ 𝑈) → ∃𝑎𝐶 (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣))
6851, 52, 66, 67syl3anc 1318 . . . 4 ((𝜑𝑣𝑉) → ∃𝑎𝐶 (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣))
6950, 68r19.29a 3060 . . 3 ((𝜑𝑣𝑉) → ∃𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
7069ralrimiva 2949 . 2 (𝜑 → ∀𝑣𝑉𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
71 iscfilu 21902 . . 3 (𝑉 ∈ (UnifOn‘𝑌) → (𝐷 ∈ (CauFilu𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣𝑉𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)))
725, 71syl 17 . 2 (𝜑 → (𝐷 ∈ (CauFilu𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣𝑉𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)))
7313, 70, 72mpbir2and 959 1 (𝜑𝐷 ∈ (CauFilu𝑉))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  wral 2896  wrex 2897  Vcvv 3173  wss 3540  cop 4131   class class class wbr 4583  cmpt 4643   × cxp 5036  ccnv 5037  ran crn 5039  cima 5041  Fun wfun 5798   Fn wfn 5799  wf 5800  cfv 5804  (class class class)co 6549  cmpt2 6551  fBascfbas 19555  UnifOncust 21813   Cnucucn 21889  CauFiluccfilu 21900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-map 7746  df-fbas 19564  df-ust 21814  df-ucn 21890  df-cfilu 21901
This theorem is referenced by:  ucnextcn  21918
  Copyright terms: Public domain W3C validator