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

Theorem fmucnd 21843
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 21840 . . . 4 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu𝑈)) → 𝐶 ∈ (fBas‘𝑋))
41, 2, 3syl2anc 690 . . 3 (𝜑𝐶 ∈ (fBas‘𝑋))
5 fmucnd.2 . . . 4 (𝜑𝑉 ∈ (UnifOn‘𝑌))
6 fmucnd.3 . . . 4 (𝜑𝐹 ∈ (𝑈 Cnu𝑉))
7 isucn 21829 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑣𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑣(𝐹𝑦)))))
87simprbda 650 . . . 4 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) ∧ 𝐹 ∈ (𝑈 Cnu𝑉)) → 𝐹:𝑋𝑌)
91, 5, 6, 8syl21anc 1316 . . 3 (𝜑𝐹:𝑋𝑌)
105elfvexd 6112 . . 3 (𝜑𝑌 ∈ V)
11 fmucnd.5 . . . 4 𝐷 = ran (𝑎𝐶 ↦ (𝐹𝑎))
1211fbasrn 21435 . . 3 ((𝐶 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌𝑌 ∈ V) → 𝐷 ∈ (fBas‘𝑌))
134, 9, 10, 12syl3anc 1317 . 2 (𝜑𝐷 ∈ (fBas‘𝑌))
14 simplr 787 . . . . . . . 8 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → 𝑎𝐶)
15 eqid 2604 . . . . . . . 8 (𝐹𝑎) = (𝐹𝑎)
16 imaeq2 5363 . . . . . . . . . 10 (𝑐 = 𝑎 → (𝐹𝑐) = (𝐹𝑎))
1716eqeq2d 2614 . . . . . . . . 9 (𝑐 = 𝑎 → ((𝐹𝑎) = (𝐹𝑐) ↔ (𝐹𝑎) = (𝐹𝑎)))
1817rspcev 3276 . . . . . . . 8 ((𝑎𝐶 ∧ (𝐹𝑎) = (𝐹𝑎)) → ∃𝑐𝐶 (𝐹𝑎) = (𝐹𝑐))
1914, 15, 18sylancl 692 . . . . . . 7 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ∃𝑐𝐶 (𝐹𝑎) = (𝐹𝑐))
20 imaexg 6967 . . . . . . . . 9 (𝐹 ∈ (𝑈 Cnu𝑉) → (𝐹𝑎) ∈ V)
21 eqid 2604 . . . . . . . . . 10 (𝑐𝐶 ↦ (𝐹𝑐)) = (𝑐𝐶 ↦ (𝐹𝑐))
2221elrnmpt 5275 . . . . . . . . 9 ((𝐹𝑎) ∈ V → ((𝐹𝑎) ∈ ran (𝑐𝐶 ↦ (𝐹𝑐)) ↔ ∃𝑐𝐶 (𝐹𝑎) = (𝐹𝑐)))
236, 20, 223syl 18 . . . . . . . 8 (𝜑 → ((𝐹𝑎) ∈ ran (𝑐𝐶 ↦ (𝐹𝑐)) ↔ ∃𝑐𝐶 (𝐹𝑎) = (𝐹𝑐)))
2423ad3antrrr 761 . . . . . . 7 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ((𝐹𝑎) ∈ ran (𝑐𝐶 ↦ (𝐹𝑐)) ↔ ∃𝑐𝐶 (𝐹𝑎) = (𝐹𝑐)))
2519, 24mpbird 245 . . . . . 6 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → (𝐹𝑎) ∈ ran (𝑐𝐶 ↦ (𝐹𝑐)))
26 imaeq2 5363 . . . . . . . . 9 (𝑎 = 𝑐 → (𝐹𝑎) = (𝐹𝑐))
2726cbvmptv 4667 . . . . . . . 8 (𝑎𝐶 ↦ (𝐹𝑎)) = (𝑐𝐶 ↦ (𝐹𝑐))
2827rneqi 5255 . . . . . . 7 ran (𝑎𝐶 ↦ (𝐹𝑎)) = ran (𝑐𝐶 ↦ (𝐹𝑐))
2911, 28eqtri 2626 . . . . . 6 𝐷 = ran (𝑐𝐶 ↦ (𝐹𝑐))
3025, 29syl6eleqr 2693 . . . . 5 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → (𝐹𝑎) ∈ 𝐷)
31 ffn 5939 . . . . . . . . 9 (𝐹:𝑋𝑌𝐹 Fn 𝑋)
329, 31syl 17 . . . . . . . 8 (𝜑𝐹 Fn 𝑋)
3332ad3antrrr 761 . . . . . . 7 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → 𝐹 Fn 𝑋)
34 simplll 793 . . . . . . . 8 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → 𝜑)
35 fbelss 21384 . . . . . . . . 9 ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑎𝐶) → 𝑎𝑋)
364, 35sylan 486 . . . . . . . 8 ((𝜑𝑎𝐶) → 𝑎𝑋)
3734, 14, 36syl2anc 690 . . . . . . 7 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → 𝑎𝑋)
38 fmucndlem 21842 . . . . . . 7 ((𝐹 Fn 𝑋𝑎𝑋) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹𝑎) × (𝐹𝑎)))
3933, 37, 38syl2anc 690 . . . . . 6 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ (𝑎 × 𝑎)) = ((𝐹𝑎) × (𝐹𝑎)))
40 eqid 2604 . . . . . . . . 9 (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) = (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩)
4140mpt2fun 6633 . . . . . . . 8 Fun (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩)
42 funimass2 5867 . . . . . . . 8 ((Fun (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
4341, 42mpan 701 . . . . . . 7 ((𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
4443adantl 480 . . . . . 6 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ (𝑎 × 𝑎)) ⊆ 𝑣)
4539, 44eqsstr3d 3597 . . . . 5 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ((𝐹𝑎) × (𝐹𝑎)) ⊆ 𝑣)
46 id 22 . . . . . . . 8 (𝑏 = (𝐹𝑎) → 𝑏 = (𝐹𝑎))
4746sqxpeqd 5050 . . . . . . 7 (𝑏 = (𝐹𝑎) → (𝑏 × 𝑏) = ((𝐹𝑎) × (𝐹𝑎)))
4847sseq1d 3589 . . . . . 6 (𝑏 = (𝐹𝑎) → ((𝑏 × 𝑏) ⊆ 𝑣 ↔ ((𝐹𝑎) × (𝐹𝑎)) ⊆ 𝑣))
4948rspcev 3276 . . . . 5 (((𝐹𝑎) ∈ 𝐷 ∧ ((𝐹𝑎) × (𝐹𝑎)) ⊆ 𝑣) → ∃𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
5030, 45, 49syl2anc 690 . . . 4 ((((𝜑𝑣𝑉) ∧ 𝑎𝐶) ∧ (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣)) → ∃𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
511adantr 479 . . . . 5 ((𝜑𝑣𝑉) → 𝑈 ∈ (UnifOn‘𝑋))
522adantr 479 . . . . 5 ((𝜑𝑣𝑉) → 𝐶 ∈ (CauFilu𝑈))
535adantr 479 . . . . . 6 ((𝜑𝑣𝑉) → 𝑉 ∈ (UnifOn‘𝑌))
546adantr 479 . . . . . 6 ((𝜑𝑣𝑉) → 𝐹 ∈ (𝑈 Cnu𝑉))
55 simpr 475 . . . . . 6 ((𝜑𝑣𝑉) → 𝑣𝑉)
56 nfcv 2745 . . . . . . 7 𝑠⟨(𝐹𝑥), (𝐹𝑦)⟩
57 nfcv 2745 . . . . . . 7 𝑡⟨(𝐹𝑥), (𝐹𝑦)⟩
58 nfcv 2745 . . . . . . 7 𝑥⟨(𝐹𝑠), (𝐹𝑡)⟩
59 nfcv 2745 . . . . . . 7 𝑦⟨(𝐹𝑠), (𝐹𝑡)⟩
60 simpl 471 . . . . . . . . 9 ((𝑥 = 𝑠𝑦 = 𝑡) → 𝑥 = 𝑠)
6160fveq2d 6087 . . . . . . . 8 ((𝑥 = 𝑠𝑦 = 𝑡) → (𝐹𝑥) = (𝐹𝑠))
62 simpr 475 . . . . . . . . 9 ((𝑥 = 𝑠𝑦 = 𝑡) → 𝑦 = 𝑡)
6362fveq2d 6087 . . . . . . . 8 ((𝑥 = 𝑠𝑦 = 𝑡) → (𝐹𝑦) = (𝐹𝑡))
6461, 63opeq12d 4337 . . . . . . 7 ((𝑥 = 𝑠𝑦 = 𝑡) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ = ⟨(𝐹𝑠), (𝐹𝑡)⟩)
6556, 57, 58, 59, 64cbvmpt2 6605 . . . . . 6 (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) = (𝑠𝑋, 𝑡𝑋 ↦ ⟨(𝐹𝑠), (𝐹𝑡)⟩)
6651, 53, 54, 55, 65ucnprima 21833 . . . . 5 ((𝜑𝑣𝑉) → ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣) ∈ 𝑈)
67 cfiluexsm 21841 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu𝑈) ∧ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣) ∈ 𝑈) → ∃𝑎𝐶 (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣))
6851, 52, 66, 67syl3anc 1317 . . . 4 ((𝜑𝑣𝑉) → ∃𝑎𝐶 (𝑎 × 𝑎) ⊆ ((𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩) “ 𝑣))
6950, 68r19.29a 3054 . . 3 ((𝜑𝑣𝑉) → ∃𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
7069ralrimiva 2943 . 2 (𝜑 → ∀𝑣𝑉𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)
71 iscfilu 21839 . . 3 (𝑉 ∈ (UnifOn‘𝑌) → (𝐷 ∈ (CauFilu𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣𝑉𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)))
725, 71syl 17 . 2 (𝜑 → (𝐷 ∈ (CauFilu𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣𝑉𝑏𝐷 (𝑏 × 𝑏) ⊆ 𝑣)))
7313, 70, 72mpbir2and 958 1 (𝜑𝐷 ∈ (CauFilu𝑉))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1975  wral 2890  wrex 2891  Vcvv 3167  wss 3534  cop 4125   class class class wbr 4572  cmpt 4632   × cxp 5021  ccnv 5022  ran crn 5024  cima 5026  Fun wfun 5779   Fn wfn 5780  wf 5781  cfv 5785  (class class class)co 6522  cmpt2 6524  fBascfbas 19496  UnifOncust 21750   Cnucucn 21826  CauFiluccfilu 21837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-rep 4688  ax-sep 4698  ax-nul 4707  ax-pow 4759  ax-pr 4823  ax-un 6819
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2456  df-mo 2457  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ne 2776  df-nel 2777  df-ral 2895  df-rex 2896  df-rab 2899  df-v 3169  df-sbc 3397  df-csb 3494  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-nul 3869  df-if 4031  df-pw 4104  df-sn 4120  df-pr 4122  df-op 4126  df-uni 4362  df-iun 4446  df-br 4573  df-opab 4633  df-mpt 4634  df-id 4938  df-xp 5029  df-rel 5030  df-cnv 5031  df-co 5032  df-dm 5033  df-rn 5034  df-res 5035  df-ima 5036  df-iota 5749  df-fun 5787  df-fn 5788  df-f 5789  df-fv 5793  df-ov 6525  df-oprab 6526  df-mpt2 6527  df-1st 7031  df-2nd 7032  df-map 7718  df-fbas 19505  df-ust 21751  df-ucn 21827  df-cfilu 21838
This theorem is referenced by:  ucnextcn  21855
  Copyright terms: Public domain W3C validator