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

Theorem fiun 7911
Description: The union of a chain (with respect to inclusion) of functions is a function. Analogous to f1iun 7912. (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 3477 . . . . . . . 8 𝑢 ∈ V
2 eqeq1 2735 . . . . . . . . 9 (𝑧 = 𝑢 → (𝑧 = 𝐵𝑢 = 𝐵))
32rexbidv 3177 . . . . . . . 8 (𝑧 = 𝑢 → (∃𝑥𝐴 𝑧 = 𝐵 ↔ ∃𝑥𝐴 𝑢 = 𝐵))
41, 3elab 3664 . . . . . . 7 (𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} ↔ ∃𝑥𝐴 𝑢 = 𝐵)
5 r19.29 3113 . . . . . . . 8 ((∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ ∃𝑥𝐴 𝑢 = 𝐵) → ∃𝑥𝐴 ((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵))
6 nfv 1917 . . . . . . . . . 10 𝑥Fun 𝑢
7 nfre1 3281 . . . . . . . . . . . 12 𝑥𝑥𝐴 𝑧 = 𝐵
87nfab 2908 . . . . . . . . . . 11 𝑥{𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}
9 nfv 1917 . . . . . . . . . . 11 𝑥(𝑢𝑣𝑣𝑢)
108, 9nfralw 3307 . . . . . . . . . 10 𝑥𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)
116, 10nfan 1902 . . . . . . . . 9 𝑥(Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢))
12 ffun 6707 . . . . . . . . . . . . 13 (𝐵:𝐷𝑆 → Fun 𝐵)
13 funeq 6557 . . . . . . . . . . . . 13 (𝑢 = 𝐵 → (Fun 𝑢 ↔ Fun 𝐵))
14 bianir 1057 . . . . . . . . . . . . 13 ((Fun 𝐵 ∧ (Fun 𝑢 ↔ Fun 𝐵)) → Fun 𝑢)
1512, 13, 14syl2an 596 . . . . . . . . . . . 12 ((𝐵:𝐷𝑆𝑢 = 𝐵) → Fun 𝑢)
1615adantlr 713 . . . . . . . . . . 11 (((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → Fun 𝑢)
17 fiun.1 . . . . . . . . . . . 12 (𝑥 = 𝑦𝐵 = 𝐶)
1817fiunlem 7910 . . . . . . . . . . 11 (((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢))
1916, 18jca 512 . . . . . . . . . 10 (((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
2019a1i 11 . . . . . . . . 9 (𝑥𝐴 → (((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢))))
2111, 20rexlimi 3255 . . . . . . . 8 (∃𝑥𝐴 ((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
225, 21syl 17 . . . . . . 7 ((∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ ∃𝑥𝐴 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
234, 22sylan2b 594 . . . . . 6 ((∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
2423ralrimiva 3145 . . . . 5 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ∀𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)))
25 fununi 6612 . . . . 5 (∀𝑢 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵} (𝑢𝑣𝑣𝑢)) → Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
2624, 25syl 17 . . . 4 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
27 fiun.2 . . . . . 6 𝐵 ∈ V
2827dfiun2 5029 . . . . 5 𝑥𝐴 𝐵 = {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵}
2928funeqi 6558 . . . 4 (Fun 𝑥𝐴 𝐵 ↔ Fun {𝑧 ∣ ∃𝑥𝐴 𝑧 = 𝐵})
3026, 29sylibr 233 . . 3 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → Fun 𝑥𝐴 𝐵)
311eldm2 5893 . . . . . . . 8 (𝑢 ∈ dom 𝐵 ↔ ∃𝑣𝑢, 𝑣⟩ ∈ 𝐵)
32 fdm 6713 . . . . . . . . 9 (𝐵:𝐷𝑆 → dom 𝐵 = 𝐷)
3332eleq2d 2818 . . . . . . . 8 (𝐵:𝐷𝑆 → (𝑢 ∈ dom 𝐵𝑢𝐷))
3431, 33bitr3id 284 . . . . . . 7 (𝐵:𝐷𝑆 → (∃𝑣𝑢, 𝑣⟩ ∈ 𝐵𝑢𝐷))
3534adantr 481 . . . . . 6 ((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (∃𝑣𝑢, 𝑣⟩ ∈ 𝐵𝑢𝐷))
3635ralrexbid 3105 . . . . 5 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (∃𝑥𝐴𝑣𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑥𝐴 𝑢𝐷))
37 eliun 4994 . . . . . . 7 (⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴𝑢, 𝑣⟩ ∈ 𝐵)
3837exbii 1850 . . . . . 6 (∃𝑣𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝐵 ↔ ∃𝑣𝑥𝐴𝑢, 𝑣⟩ ∈ 𝐵)
391eldm2 5893 . . . . . 6 (𝑢 ∈ dom 𝑥𝐴 𝐵 ↔ ∃𝑣𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝐵)
40 rexcom4 3284 . . . . . 6 (∃𝑥𝐴𝑣𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑣𝑥𝐴𝑢, 𝑣⟩ ∈ 𝐵)
4138, 39, 403bitr4i 302 . . . . 5 (𝑢 ∈ dom 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴𝑣𝑢, 𝑣⟩ ∈ 𝐵)
42 eliun 4994 . . . . 5 (𝑢 𝑥𝐴 𝐷 ↔ ∃𝑥𝐴 𝑢𝐷)
4336, 41, 423bitr4g 313 . . . 4 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → (𝑢 ∈ dom 𝑥𝐴 𝐵𝑢 𝑥𝐴 𝐷))
4443eqrdv 2729 . . 3 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → dom 𝑥𝐴 𝐵 = 𝑥𝐴 𝐷)
45 df-fn 6535 . . 3 ( 𝑥𝐴 𝐵 Fn 𝑥𝐴 𝐷 ↔ (Fun 𝑥𝐴 𝐵 ∧ dom 𝑥𝐴 𝐵 = 𝑥𝐴 𝐷))
4630, 44, 45sylanbrc 583 . 2 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 𝐵 Fn 𝑥𝐴 𝐷)
47 rniun 6136 . . 3 ran 𝑥𝐴 𝐵 = 𝑥𝐴 ran 𝐵
48 frn 6711 . . . . . 6 (𝐵:𝐷𝑆 → ran 𝐵𝑆)
4948adantr 481 . . . . 5 ((𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ran 𝐵𝑆)
5049ralimi 3082 . . . 4 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ∀𝑥𝐴 ran 𝐵𝑆)
51 iunss 5041 . . . 4 ( 𝑥𝐴 ran 𝐵𝑆 ↔ ∀𝑥𝐴 ran 𝐵𝑆)
5250, 51sylibr 233 . . 3 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 ran 𝐵𝑆)
5347, 52eqsstrid 4026 . 2 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → ran 𝑥𝐴 𝐵𝑆)
54 df-f 6536 . 2 ( 𝑥𝐴 𝐵: 𝑥𝐴 𝐷𝑆 ↔ ( 𝑥𝐴 𝐵 Fn 𝑥𝐴 𝐷 ∧ ran 𝑥𝐴 𝐵𝑆))
5546, 53, 54sylanbrc 583 1 (∀𝑥𝐴 (𝐵:𝐷𝑆 ∧ ∀𝑦𝐴 (𝐵𝐶𝐶𝐵)) → 𝑥𝐴 𝐵: 𝑥𝐴 𝐷𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wex 1781  wcel 2106  {cab 2708  wral 3060  wrex 3069  Vcvv 3473  wss 3944  cop 4628   cuni 4901   ciun 4990  dom cdm 5669  ran crn 5670  Fun wfun 6526   Fn wfn 6527  wf 6528
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4992  df-br 5142  df-opab 5204  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-fun 6534  df-fn 6535  df-f 6536
This theorem is referenced by:  satfun  34233
  Copyright terms: Public domain W3C validator