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

Theorem fiun 7716
Description: The union of a chain (with respect to inclusion) of functions is a function. Analogous to f1iun 7717. (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 3412 . . . . . . . 8 𝑢 ∈ V
2 eqeq1 2741 . . . . . . . . 9 (𝑧 = 𝑢 → (𝑧 = 𝐵𝑢 = 𝐵))
32rexbidv 3216 . . . . . . . 8 (𝑧 = 𝑢 → (∃𝑥𝐴 𝑧 = 𝐵 ↔ ∃𝑥𝐴 𝑢 = 𝐵))
41, 3elab 3587 . . . . . . 7 (𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} ↔ ∃𝑥𝐴 𝑢 = 𝐵)
5 r19.29 3176 . . . . . . . 8 ((∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ ∃𝑥𝐴 𝑢 = 𝐵) → ∃𝑥𝐴 ((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵))
6 nfv 1922 . . . . . . . . . 10 𝑥Fun 𝑢
7 nfre1 3225 . . . . . . . . . . . 12 𝑥𝑥𝐴 𝑧 = 𝐵
87nfab 2910 . . . . . . . . . . 11 𝑥{𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}
9 nfv 1922 . . . . . . . . . . 11 𝑥(𝑢𝑣𝑣𝑢)
108, 9nfralw 3147 . . . . . . . . . 10 𝑥𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)
116, 10nfan 1907 . . . . . . . . 9 𝑥(Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢))
12 ffun 6548 . . . . . . . . . . . . 13 (𝐵:𝐷𝑆 → Fun 𝐵)
13 funeq 6400 . . . . . . . . . . . . 13 (𝑢 = 𝐵 → (Fun 𝑢 ↔ Fun 𝐵))
14 bianir 1059 . . . . . . . . . . . . 13 ((Fun 𝐵 ∧ (Fun 𝑢 ↔ Fun 𝐵)) → Fun 𝑢)
1512, 13, 14syl2an 599 . . . . . . . . . . . 12 ((𝐵:𝐷𝑆𝑢 = 𝐵) → Fun 𝑢)
1615adantlr 715 . . . . . . . . . . 11 (((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → Fun 𝑢)
17 fiun.1 . . . . . . . . . . . 12 (𝑥 = 𝑦𝐵 = 𝐶)
1817fiunlem 7715 . . . . . . . . . . 11 (((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢))
1916, 18jca 515 . . . . . . . . . 10 (((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
2019a1i 11 . . . . . . . . 9 (𝑥𝐴 → (((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢))))
2111, 20rexlimi 3234 . . . . . . . 8 (∃𝑥𝐴 ((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
225, 21syl 17 . . . . . . 7 ((∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ ∃𝑥𝐴 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
234, 22sylan2b 597 . . . . . 6 ((∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
2423ralrimiva 3105 . . . . 5 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ∀𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
25 fununi 6455 . . . . 5 (∀𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)) → Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
2624, 25syl 17 . . . 4 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
27 fiun.2 . . . . . 6 𝐵 ∈ V
2827dfiun2 4942 . . . . 5 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}
2928funeqi 6401 . . . 4 (Fun 𝑥𝐴 𝐵 ↔ Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
3026, 29sylibr 237 . . 3 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → Fun 𝑥𝐴 𝐵)
311eldm2 5770 . . . . . . . 8 (𝑢 ∈ dom 𝐵 ↔ ∃𝑣𝑢, 𝑣⟩ ∈ 𝐵)
32 fdm 6554 . . . . . . . . 9 (𝐵:𝐷𝑆 → dom 𝐵 = 𝐷)
3332eleq2d 2823 . . . . . . . 8 (𝐵:𝐷𝑆 → (𝑢 ∈ dom 𝐵𝑢𝐷))
3431, 33bitr3id 288 . . . . . . 7 (𝐵:𝐷𝑆 → (∃𝑣𝑢, 𝑣⟩ ∈ 𝐵𝑢𝐷))
3534adantr 484 . . . . . 6 ((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (∃𝑣𝑢, 𝑣⟩ ∈ 𝐵𝑢𝐷))
3635ralrexbid 3241 . . . . 5 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (∃𝑥𝐴𝑣𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑥𝐴 𝑢𝐷))
37 eliun 4908 . . . . . . 7 (⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴𝑢, 𝑣⟩ ∈ 𝐵)
3837exbii 1855 . . . . . 6 (∃𝑣𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝐵 ↔ ∃𝑣𝑥𝐴𝑢, 𝑣⟩ ∈ 𝐵)
391eldm2 5770 . . . . . 6 (𝑢 ∈ dom 𝑥𝐴 𝐵 ↔ ∃𝑣𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝐵)
40 rexcom4 3172 . . . . . 6 (∃𝑥𝐴𝑣𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑣𝑥𝐴𝑢, 𝑣⟩ ∈ 𝐵)
4138, 39, 403bitr4i 306 . . . . 5 (𝑢 ∈ dom 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴𝑣𝑢, 𝑣⟩ ∈ 𝐵)
42 eliun 4908 . . . . 5 (𝑢 𝑥𝐴 𝐷 ↔ ∃𝑥𝐴 𝑢𝐷)
4336, 41, 423bitr4g 317 . . . 4 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (𝑢 ∈ dom 𝑥𝐴 𝐵𝑢 𝑥𝐴 𝐷))
4443eqrdv 2735 . . 3 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → dom 𝑥𝐴 𝐵 = 𝑥𝐴 𝐷)
45 df-fn 6383 . . 3 ( 𝑥𝐴 𝐵 Fn 𝑥𝐴 𝐷 ↔ (Fun 𝑥𝐴 𝐵 ∧ dom 𝑥𝐴 𝐵 = 𝑥𝐴 𝐷))
4630, 44, 45sylanbrc 586 . 2 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 𝐵 Fn 𝑥𝐴 𝐷)
47 rniun 6011 . . 3 ran 𝑥𝐴 𝐵 = 𝑥𝐴 ran 𝐵
48 frn 6552 . . . . . 6 (𝐵:𝐷𝑆 → ran 𝐵𝑆)
4948adantr 484 . . . . 5 ((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ran 𝐵𝑆)
5049ralimi 3083 . . . 4 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ∀𝑥𝐴 ran 𝐵𝑆)
51 iunss 4954 . . . 4 ( 𝑥𝐴 ran 𝐵𝑆 ↔ ∀𝑥𝐴 ran 𝐵𝑆)
5250, 51sylibr 237 . . 3 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 ran 𝐵𝑆)
5347, 52eqsstrid 3949 . 2 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ran 𝑥𝐴 𝐵𝑆)
54 df-f 6384 . 2 ( 𝑥𝐴 𝐵: 𝑥𝐴 𝐷𝑆 ↔ ( 𝑥𝐴 𝐵 Fn 𝑥𝐴 𝐷 ∧ ran 𝑥𝐴 𝐵𝑆))
5546, 53, 54sylanbrc 586 1 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 𝐵: 𝑥𝐴 𝐷𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 847   = wceq 1543  wex 1787  wcel 2110  {cab 2714  wral 3061  wrex 3062  Vcvv 3408  wss 3866  cop 4547   cuni 4819   ciun 4904  dom cdm 5551  ran crn 5552  Fun wfun 6374   Fn wfn 6375  wf 6376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-id 5455  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-fun 6382  df-fn 6383  df-f 6384
This theorem is referenced by:  satfun  33086
  Copyright terms: Public domain W3C validator