Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj882 Structured version   Visualization version   GIF version

Theorem bnj882 31328
Description: Definition (using hypotheses for readability) of the function giving the transitive closure of 𝑋 in 𝐴 by 𝑅. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj882.1 (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
bnj882.2 (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
bnj882.3 𝐷 = (ω ∖ {∅})
bnj882.4 𝐵 = {𝑓 ∣ ∃𝑛𝐷 (𝑓 Fn 𝑛𝜑𝜓)}
Assertion
Ref Expression
bnj882 trCl(𝑋, 𝐴, 𝑅) = 𝑓𝐵 𝑖 ∈ dom 𝑓(𝑓𝑖)
Distinct variable groups:   𝐴,𝑓,𝑖,𝑛,𝑦   𝑅,𝑓,𝑖,𝑛,𝑦   𝑓,𝑋,𝑖,𝑛,𝑦
Allowed substitution hints:   𝜑(𝑦,𝑓,𝑖,𝑛)   𝜓(𝑦,𝑓,𝑖,𝑛)   𝐵(𝑦,𝑓,𝑖,𝑛)   𝐷(𝑦,𝑓,𝑖,𝑛)

Proof of Theorem bnj882
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 df-bnj18 31095 . 2 trCl(𝑋, 𝐴, 𝑅) = 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))} 𝑖 ∈ dom 𝑓(𝑓𝑖)
2 df-iun 4654 . . 3 𝑓𝐵 𝑖 ∈ dom 𝑓(𝑓𝑖) = {𝑤 ∣ ∃𝑓𝐵 𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖)}
3 df-iun 4654 . . . 4 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))} 𝑖 ∈ dom 𝑓(𝑓𝑖) = {𝑤 ∣ ∃𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))}𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖)}
4 bnj882.4 . . . . . . . . 9 𝐵 = {𝑓 ∣ ∃𝑛𝐷 (𝑓 Fn 𝑛𝜑𝜓)}
5 bnj882.3 . . . . . . . . . . 11 𝐷 = (ω ∖ {∅})
6 bnj882.1 . . . . . . . . . . . . . 14 (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
7 bnj882.2 . . . . . . . . . . . . . 14 (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))
86, 7anbi12i 604 . . . . . . . . . . . . 13 ((𝜑𝜓) ↔ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅))))
98anbi2i 601 . . . . . . . . . . . 12 ((𝑓 Fn 𝑛 ∧ (𝜑𝜓)) ↔ (𝑓 Fn 𝑛 ∧ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))))
10 3anass 1079 . . . . . . . . . . . 12 ((𝑓 Fn 𝑛𝜑𝜓) ↔ (𝑓 Fn 𝑛 ∧ (𝜑𝜓)))
11 3anass 1079 . . . . . . . . . . . 12 ((𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ (𝑓 Fn 𝑛 ∧ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))))
129, 10, 113bitr4i 292 . . . . . . . . . . 11 ((𝑓 Fn 𝑛𝜑𝜓) ↔ (𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅))))
135, 12rexeqbii 3201 . . . . . . . . . 10 (∃𝑛𝐷 (𝑓 Fn 𝑛𝜑𝜓) ↔ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅))))
1413abbii 2887 . . . . . . . . 9 {𝑓 ∣ ∃𝑛𝐷 (𝑓 Fn 𝑛𝜑𝜓)} = {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))}
154, 14eqtri 2792 . . . . . . . 8 𝐵 = {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))}
1615eleq2i 2841 . . . . . . 7 (𝑓𝐵𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))})
1716anbi1i 602 . . . . . 6 ((𝑓𝐵𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖)) ↔ (𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))} ∧ 𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖)))
1817rexbii2 3186 . . . . 5 (∃𝑓𝐵 𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖) ↔ ∃𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))}𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖))
1918abbii 2887 . . . 4 {𝑤 ∣ ∃𝑓𝐵 𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖)} = {𝑤 ∣ ∃𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))}𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖)}
203, 19eqtr4i 2795 . . 3 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))} 𝑖 ∈ dom 𝑓(𝑓𝑖) = {𝑤 ∣ ∃𝑓𝐵 𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖)}
212, 20eqtr4i 2795 . 2 𝑓𝐵 𝑖 ∈ dom 𝑓(𝑓𝑖) = 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))} 𝑖 ∈ dom 𝑓(𝑓𝑖)
221, 21eqtr4i 2795 1 trCl(𝑋, 𝐴, 𝑅) = 𝑓𝐵 𝑖 ∈ dom 𝑓(𝑓𝑖)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1070   = wceq 1630  wcel 2144  {cab 2756  wral 3060  wrex 3061  cdif 3718  c0 4061  {csn 4314   ciun 4652  dom cdm 5249  suc csuc 5868   Fn wfn 6026  cfv 6031  ωcom 7211   predc-bnj14 31088   trClc-bnj18 31094
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-rex 3066  df-iun 4654  df-bnj18 31095
This theorem is referenced by:  bnj893  31330  bnj906  31332  bnj916  31335  bnj983  31353  bnj1014  31362  bnj1145  31393  bnj1318  31425
  Copyright terms: Public domain W3C validator