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

Theorem bnj1445 33003
Description: Technical lemma for bnj60 33021. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj1445.1 𝐵 = {𝑑 ∣ (𝑑𝐴 ∧ ∀𝑥𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)}
bnj1445.2 𝑌 = ⟨𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))⟩
bnj1445.3 𝐶 = {𝑓 ∣ ∃𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))}
bnj1445.4 (𝜏 ↔ (𝑓𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))
bnj1445.5 𝐷 = {𝑥𝐴 ∣ ¬ ∃𝑓𝜏}
bnj1445.6 (𝜓 ↔ (𝑅 FrSe 𝐴𝐷 ≠ ∅))
bnj1445.7 (𝜒 ↔ (𝜓𝑥𝐷 ∧ ∀𝑦𝐷 ¬ 𝑦𝑅𝑥))
bnj1445.8 (𝜏′[𝑦 / 𝑥]𝜏)
bnj1445.9 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}
bnj1445.10 𝑃 = 𝐻
bnj1445.11 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩
bnj1445.12 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺𝑍)⟩})
bnj1445.13 𝑊 = ⟨𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))⟩
bnj1445.14 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))
bnj1445.15 (𝜒𝑃 Fn trCl(𝑥, 𝐴, 𝑅))
bnj1445.16 (𝜒𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))
bnj1445.17 (𝜃 ↔ (𝜒𝑧𝐸))
bnj1445.18 (𝜂 ↔ (𝜃𝑧 ∈ {𝑥}))
bnj1445.19 (𝜁 ↔ (𝜃𝑧 ∈ trCl(𝑥, 𝐴, 𝑅)))
bnj1445.20 (𝜌 ↔ (𝜁𝑓𝐻𝑧 ∈ dom 𝑓))
bnj1445.21 (𝜎 ↔ (𝜌𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))))
bnj1445.22 (𝜑 ↔ (𝜎𝑑𝐵𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌)))
bnj1445.23 𝑋 = ⟨𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))⟩
Assertion
Ref Expression
bnj1445 (𝜎 → ∀𝑑𝜎)
Distinct variable groups:   𝐴,𝑑,𝑥   𝐵,𝑓   𝐸,𝑑   𝑅,𝑑,𝑥   𝑓,𝑑,𝑥   𝑦,𝑑,𝑥   𝑧,𝑑
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜓(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜒(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜃(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜏(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜂(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜁(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜎(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜌(𝑥,𝑦,𝑧,𝑓,𝑑)   𝐴(𝑦,𝑧,𝑓)   𝐵(𝑥,𝑦,𝑧,𝑑)   𝐶(𝑥,𝑦,𝑧,𝑓,𝑑)   𝐷(𝑥,𝑦,𝑧,𝑓,𝑑)   𝑃(𝑥,𝑦,𝑧,𝑓,𝑑)   𝑄(𝑥,𝑦,𝑧,𝑓,𝑑)   𝑅(𝑦,𝑧,𝑓)   𝐸(𝑥,𝑦,𝑧,𝑓)   𝐺(𝑥,𝑦,𝑧,𝑓,𝑑)   𝐻(𝑥,𝑦,𝑧,𝑓,𝑑)   𝑊(𝑥,𝑦,𝑧,𝑓,𝑑)   𝑋(𝑥,𝑦,𝑧,𝑓,𝑑)   𝑌(𝑥,𝑦,𝑧,𝑓,𝑑)   𝑍(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜏′(𝑥,𝑦,𝑧,𝑓,𝑑)

Proof of Theorem bnj1445
StepHypRef Expression
1 bnj1445.21 . 2 (𝜎 ↔ (𝜌𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))))
2 bnj1445.20 . . . . 5 (𝜌 ↔ (𝜁𝑓𝐻𝑧 ∈ dom 𝑓))
3 bnj1445.19 . . . . . . 7 (𝜁 ↔ (𝜃𝑧 ∈ trCl(𝑥, 𝐴, 𝑅)))
4 bnj1445.17 . . . . . . . . 9 (𝜃 ↔ (𝜒𝑧𝐸))
5 bnj1445.7 . . . . . . . . . . . . 13 (𝜒 ↔ (𝜓𝑥𝐷 ∧ ∀𝑦𝐷 ¬ 𝑦𝑅𝑥))
6 bnj1445.6 . . . . . . . . . . . . . . 15 (𝜓 ↔ (𝑅 FrSe 𝐴𝐷 ≠ ∅))
7 nfv 1920 . . . . . . . . . . . . . . . 16 𝑑 𝑅 FrSe 𝐴
8 bnj1445.5 . . . . . . . . . . . . . . . . . 18 𝐷 = {𝑥𝐴 ∣ ¬ ∃𝑓𝜏}
9 bnj1445.4 . . . . . . . . . . . . . . . . . . . . . 22 (𝜏 ↔ (𝑓𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))
10 bnj1445.3 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐶 = {𝑓 ∣ ∃𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))}
11 nfre1 3236 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑑𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))
1211nfab 2914 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑑{𝑓 ∣ ∃𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))}
1310, 12nfcxfr 2906 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑑𝐶
1413nfcri 2895 . . . . . . . . . . . . . . . . . . . . . . 23 𝑑 𝑓𝐶
15 nfv 1920 . . . . . . . . . . . . . . . . . . . . . . 23 𝑑dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))
1614, 15nfan 1905 . . . . . . . . . . . . . . . . . . . . . 22 𝑑(𝑓𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))
179, 16nfxfr 1858 . . . . . . . . . . . . . . . . . . . . 21 𝑑𝜏
1817nfex 2321 . . . . . . . . . . . . . . . . . . . 20 𝑑𝑓𝜏
1918nfn 1863 . . . . . . . . . . . . . . . . . . 19 𝑑 ¬ ∃𝑓𝜏
20 nfcv 2908 . . . . . . . . . . . . . . . . . . 19 𝑑𝐴
2119, 20nfrabw 3316 . . . . . . . . . . . . . . . . . 18 𝑑{𝑥𝐴 ∣ ¬ ∃𝑓𝜏}
228, 21nfcxfr 2906 . . . . . . . . . . . . . . . . 17 𝑑𝐷
23 nfcv 2908 . . . . . . . . . . . . . . . . 17 𝑑
2422, 23nfne 3046 . . . . . . . . . . . . . . . 16 𝑑 𝐷 ≠ ∅
257, 24nfan 1905 . . . . . . . . . . . . . . 15 𝑑(𝑅 FrSe 𝐴𝐷 ≠ ∅)
266, 25nfxfr 1858 . . . . . . . . . . . . . 14 𝑑𝜓
2722nfcri 2895 . . . . . . . . . . . . . 14 𝑑 𝑥𝐷
28 nfv 1920 . . . . . . . . . . . . . . 15 𝑑 ¬ 𝑦𝑅𝑥
2922, 28nfralw 3151 . . . . . . . . . . . . . 14 𝑑𝑦𝐷 ¬ 𝑦𝑅𝑥
3026, 27, 29nf3an 1907 . . . . . . . . . . . . 13 𝑑(𝜓𝑥𝐷 ∧ ∀𝑦𝐷 ¬ 𝑦𝑅𝑥)
315, 30nfxfr 1858 . . . . . . . . . . . 12 𝑑𝜒
3231nf5ri 2191 . . . . . . . . . . 11 (𝜒 → ∀𝑑𝜒)
3332bnj1351 32785 . . . . . . . . . 10 ((𝜒𝑧𝐸) → ∀𝑑(𝜒𝑧𝐸))
3433nf5i 2145 . . . . . . . . 9 𝑑(𝜒𝑧𝐸)
354, 34nfxfr 1858 . . . . . . . 8 𝑑𝜃
36 nfv 1920 . . . . . . . 8 𝑑 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅)
3735, 36nfan 1905 . . . . . . 7 𝑑(𝜃𝑧 ∈ trCl(𝑥, 𝐴, 𝑅))
383, 37nfxfr 1858 . . . . . 6 𝑑𝜁
39 bnj1445.9 . . . . . . . 8 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}
40 nfcv 2908 . . . . . . . . . 10 𝑑 pred(𝑥, 𝐴, 𝑅)
41 bnj1445.8 . . . . . . . . . . 11 (𝜏′[𝑦 / 𝑥]𝜏)
42 nfcv 2908 . . . . . . . . . . . 12 𝑑𝑦
4342, 17nfsbcw 3741 . . . . . . . . . . 11 𝑑[𝑦 / 𝑥]𝜏
4441, 43nfxfr 1858 . . . . . . . . . 10 𝑑𝜏′
4540, 44nfrex 3239 . . . . . . . . 9 𝑑𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′
4645nfab 2914 . . . . . . . 8 𝑑{𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}
4739, 46nfcxfr 2906 . . . . . . 7 𝑑𝐻
4847nfcri 2895 . . . . . 6 𝑑 𝑓𝐻
49 nfv 1920 . . . . . 6 𝑑 𝑧 ∈ dom 𝑓
5038, 48, 49nf3an 1907 . . . . 5 𝑑(𝜁𝑓𝐻𝑧 ∈ dom 𝑓)
512, 50nfxfr 1858 . . . 4 𝑑𝜌
5251nf5ri 2191 . . 3 (𝜌 → ∀𝑑𝜌)
53 ax-5 1916 . . 3 (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) → ∀𝑑 𝑦 ∈ pred(𝑥, 𝐴, 𝑅))
5414nf5ri 2191 . . 3 (𝑓𝐶 → ∀𝑑 𝑓𝐶)
55 ax-5 1916 . . 3 (dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)) → ∀𝑑dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)))
5652, 53, 54, 55bnj982 32737 . 2 ((𝜌𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))) → ∀𝑑(𝜌𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))))
571, 56hbxfrbi 1830 1 (𝜎 → ∀𝑑𝜎)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1085  wal 1539   = wceq 1541  wex 1785  wcel 2109  {cab 2716  wne 2944  wral 3065  wrex 3066  {crab 3069  [wsbc 3719  cun 3889  wss 3891  c0 4261  {csn 4566  cop 4572   cuni 4844   class class class wbr 5078  dom cdm 5588  cres 5590   Fn wfn 6425  cfv 6430  w-bnj17 32644   predc-bnj14 32646   FrSe w-bnj15 32650   trClc-bnj18 32652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-ex 1786  df-nf 1790  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-sbc 3720  df-bnj17 32645
This theorem is referenced by:  bnj1450  33009
  Copyright terms: Public domain W3C validator