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 32619
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 32386 . 2 trCl(𝑋, 𝐴, 𝑅) = 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))} 𝑖 ∈ dom 𝑓(𝑓𝑖)
2 df-iun 4906 . . 3 𝑓𝐵 𝑖 ∈ dom 𝑓(𝑓𝑖) = {𝑤 ∣ ∃𝑓𝐵 𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖)}
3 df-iun 4906 . . . 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 630 . . . . . . . . . . . . 13 ((𝜑𝜓) ↔ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅))))
98anbi2i 626 . . . . . . . . . . . 12 ((𝑓 Fn 𝑛 ∧ (𝜑𝜓)) ↔ (𝑓 Fn 𝑛 ∧ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))))
10 3anass 1097 . . . . . . . . . . . 12 ((𝑓 Fn 𝑛𝜑𝜓) ↔ (𝑓 Fn 𝑛 ∧ (𝜑𝜓)))
11 3anass 1097 . . . . . . . . . . . 12 ((𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅))) ↔ (𝑓 Fn 𝑛 ∧ ((𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))))
129, 10, 113bitr4i 306 . . . . . . . . . . 11 ((𝑓 Fn 𝑛𝜑𝜓) ↔ (𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅))))
135, 12rexeqbii 3245 . . . . . . . . . 10 (∃𝑛𝐷 (𝑓 Fn 𝑛𝜑𝜓) ↔ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅))))
1413abbii 2808 . . . . . . . . 9 {𝑓 ∣ ∃𝑛𝐷 (𝑓 Fn 𝑛𝜑𝜓)} = {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))}
154, 14eqtri 2765 . . . . . . . 8 𝐵 = {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))}
1615eleq2i 2829 . . . . . . 7 (𝑓𝐵𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))})
1716anbi1i 627 . . . . . 6 ((𝑓𝐵𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖)) ↔ (𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))} ∧ 𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖)))
1817rexbii2 3168 . . . . 5 (∃𝑓𝐵 𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖) ↔ ∃𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))}𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖))
1918abbii 2808 . . . 4 {𝑤 ∣ ∃𝑓𝐵 𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖)} = {𝑤 ∣ ∃𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))}𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖)}
203, 19eqtr4i 2768 . . 3 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))} 𝑖 ∈ dom 𝑓(𝑓𝑖) = {𝑤 ∣ ∃𝑓𝐵 𝑤 𝑖 ∈ dom 𝑓(𝑓𝑖)}
212, 20eqtr4i 2768 . 2 𝑓𝐵 𝑖 ∈ dom 𝑓(𝑓𝑖) = 𝑓 ∈ {𝑓 ∣ ∃𝑛 ∈ (ω ∖ {∅})(𝑓 Fn 𝑛 ∧ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅) ∧ ∀𝑖 ∈ ω (suc 𝑖𝑛 → (𝑓‘suc 𝑖) = 𝑦 ∈ (𝑓𝑖) pred(𝑦, 𝐴, 𝑅)))} 𝑖 ∈ dom 𝑓(𝑓𝑖)
221, 21eqtr4i 2768 1 trCl(𝑋, 𝐴, 𝑅) = 𝑓𝐵 𝑖 ∈ dom 𝑓(𝑓𝑖)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089   = wceq 1543  wcel 2110  {cab 2714  wral 3061  wrex 3062  cdif 3863  c0 4237  {csn 4541   ciun 4904  dom cdm 5551  suc csuc 6215   Fn wfn 6375  cfv 6380  ωcom 7644   predc-bnj14 32379   trClc-bnj18 32385
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-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3067  df-iun 4906  df-bnj18 32386
This theorem is referenced by:  bnj893  32621  bnj906  32623  bnj916  32626  bnj983  32644  bnj1014  32654  bnj1145  32686  bnj1318  32718
  Copyright terms: Public domain W3C validator