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

Theorem fiun 7922
Description: The union of a chain (with respect to inclusion) of functions is a function. Analogous to f1iun 7923. (Contributed by AV, 6-Oct-2023.)
Hypotheses
Ref Expression
fiun.1 (𝑥 = 𝑦𝐵 = 𝐶)
fiun.2 𝐵 ∈ V
Assertion
Ref Expression
fiun (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 𝐵: 𝑥𝐴 𝐷𝑆)
Distinct variable groups:   𝑥,𝐴,𝑦   𝑦,𝐵   𝑥,𝐶   𝑥,𝑦   𝑥,𝑆
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑦)   𝐷(𝑥,𝑦)   𝑆(𝑦)

Proof of Theorem fiun
Dummy variables 𝑣 𝑧 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3470 . . . . . . . 8 𝑢 ∈ V
2 eqeq1 2728 . . . . . . . . 9 (𝑧 = 𝑢 → (𝑧 = 𝐵𝑢 = 𝐵))
32rexbidv 3170 . . . . . . . 8 (𝑧 = 𝑢 → (∃𝑥𝐴 𝑧 = 𝐵 ↔ ∃𝑥𝐴 𝑢 = 𝐵))
41, 3elab 3660 . . . . . . 7 (𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} ↔ ∃𝑥𝐴 𝑢 = 𝐵)
5 r19.29 3106 . . . . . . . 8 ((∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ ∃𝑥𝐴 𝑢 = 𝐵) → ∃𝑥𝐴 ((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵))
6 nfv 1909 . . . . . . . . . 10 𝑥Fun 𝑢
7 nfre1 3274 . . . . . . . . . . . 12 𝑥𝑥𝐴 𝑧 = 𝐵
87nfab 2901 . . . . . . . . . . 11 𝑥{𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}
9 nfv 1909 . . . . . . . . . . 11 𝑥(𝑢𝑣𝑣𝑢)
108, 9nfralw 3300 . . . . . . . . . 10 𝑥𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)
116, 10nfan 1894 . . . . . . . . 9 𝑥(Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢))
12 ffun 6710 . . . . . . . . . . . . 13 (𝐵:𝐷𝑆 → Fun 𝐵)
13 funeq 6558 . . . . . . . . . . . . 13 (𝑢 = 𝐵 → (Fun 𝑢 ↔ Fun 𝐵))
14 bianir 1055 . . . . . . . . . . . . 13 ((Fun 𝐵 ∧ (Fun 𝑢 ↔ Fun 𝐵)) → Fun 𝑢)
1512, 13, 14syl2an 595 . . . . . . . . . . . 12 ((𝐵:𝐷𝑆𝑢 = 𝐵) → Fun 𝑢)
1615adantlr 712 . . . . . . . . . . 11 (((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → Fun 𝑢)
17 fiun.1 . . . . . . . . . . . 12 (𝑥 = 𝑦𝐵 = 𝐶)
1817fiunlem 7921 . . . . . . . . . . 11 (((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢))
1916, 18jca 511 . . . . . . . . . 10 (((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
2019a1i 11 . . . . . . . . 9 (𝑥𝐴 → (((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢))))
2111, 20rexlimi 3248 . . . . . . . 8 (∃𝑥𝐴 ((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
225, 21syl 17 . . . . . . 7 ((∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ ∃𝑥𝐴 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
234, 22sylan2b 593 . . . . . 6 ((∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
2423ralrimiva 3138 . . . . 5 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ∀𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
25 fununi 6613 . . . . 5 (∀𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)) → Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
2624, 25syl 17 . . . 4 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
27 fiun.2 . . . . . 6 𝐵 ∈ V
2827dfiun2 5026 . . . . 5 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}
2928funeqi 6559 . . . 4 (Fun 𝑥𝐴 𝐵 ↔ Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
3026, 29sylibr 233 . . 3 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → Fun 𝑥𝐴 𝐵)
311eldm2 5891 . . . . . . . 8 (𝑢 ∈ dom 𝐵 ↔ ∃𝑣𝑢, 𝑣⟩ ∈ 𝐵)
32 fdm 6716 . . . . . . . . 9 (𝐵:𝐷𝑆 → dom 𝐵 = 𝐷)
3332eleq2d 2811 . . . . . . . 8 (𝐵:𝐷𝑆 → (𝑢 ∈ dom 𝐵𝑢𝐷))
3431, 33bitr3id 285 . . . . . . 7 (𝐵:𝐷𝑆 → (∃𝑣𝑢, 𝑣⟩ ∈ 𝐵𝑢𝐷))
3534adantr 480 . . . . . 6 ((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (∃𝑣𝑢, 𝑣⟩ ∈ 𝐵𝑢𝐷))
3635ralrexbid 3098 . . . . 5 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (∃𝑥𝐴𝑣𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑥𝐴 𝑢𝐷))
37 eliun 4991 . . . . . . 7 (⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴𝑢, 𝑣⟩ ∈ 𝐵)
3837exbii 1842 . . . . . 6 (∃𝑣𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝐵 ↔ ∃𝑣𝑥𝐴𝑢, 𝑣⟩ ∈ 𝐵)
391eldm2 5891 . . . . . 6 (𝑢 ∈ dom 𝑥𝐴 𝐵 ↔ ∃𝑣𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝐵)
40 rexcom4 3277 . . . . . 6 (∃𝑥𝐴𝑣𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑣𝑥𝐴𝑢, 𝑣⟩ ∈ 𝐵)
4138, 39, 403bitr4i 303 . . . . 5 (𝑢 ∈ dom 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴𝑣𝑢, 𝑣⟩ ∈ 𝐵)
42 eliun 4991 . . . . 5 (𝑢 𝑥𝐴 𝐷 ↔ ∃𝑥𝐴 𝑢𝐷)
4336, 41, 423bitr4g 314 . . . 4 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (𝑢 ∈ dom 𝑥𝐴 𝐵𝑢 𝑥𝐴 𝐷))
4443eqrdv 2722 . . 3 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → dom 𝑥𝐴 𝐵 = 𝑥𝐴 𝐷)
45 df-fn 6536 . . 3 ( 𝑥𝐴 𝐵 Fn 𝑥𝐴 𝐷 ↔ (Fun 𝑥𝐴 𝐵 ∧ dom 𝑥𝐴 𝐵 = 𝑥𝐴 𝐷))
4630, 44, 45sylanbrc 582 . 2 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 𝐵 Fn 𝑥𝐴 𝐷)
47 rniun 6137 . . 3 ran 𝑥𝐴 𝐵 = 𝑥𝐴 ran 𝐵
48 frn 6714 . . . . . 6 (𝐵:𝐷𝑆 → ran 𝐵𝑆)
4948adantr 480 . . . . 5 ((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ran 𝐵𝑆)
5049ralimi 3075 . . . 4 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ∀𝑥𝐴 ran 𝐵𝑆)
51 iunss 5038 . . . 4 ( 𝑥𝐴 ran 𝐵𝑆 ↔ ∀𝑥𝐴 ran 𝐵𝑆)
5250, 51sylibr 233 . . 3 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 ran 𝐵𝑆)
5347, 52eqsstrid 4022 . 2 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ran 𝑥𝐴 𝐵𝑆)
54 df-f 6537 . 2 ( 𝑥𝐴 𝐵: 𝑥𝐴 𝐷𝑆 ↔ ( 𝑥𝐴 𝐵 Fn 𝑥𝐴 𝐷 ∧ ran 𝑥𝐴 𝐵𝑆))
5546, 53, 54sylanbrc 582 1 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 𝐵: 𝑥𝐴 𝐷𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wo 844   = wceq 1533  wex 1773  wcel 2098  {cab 2701  wral 3053  wrex 3062  Vcvv 3466  wss 3940  cop 4626   cuni 4899   ciun 4987  dom cdm 5666  ran crn 5667  Fun wfun 6527   Fn wfn 6528  wf 6529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-fun 6535  df-fn 6536  df-f 6537
This theorem is referenced by:  satfun  34891
  Copyright terms: Public domain W3C validator