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 32213
Description: Technical lemma for bnj60 32231. 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 1906 . . . . . . . . . . . . . . . 16 𝑑 𝑅 FrSe 𝐴
8 bnj1445.5 . . . . . . . . . . . . . . . . . 18 𝐷 = {𝑥𝐴 ∣ ¬ ∃𝑓𝜏}
9 bnj1445.4 . . . . . . . . . . . . . . . . . . . . . 22 (𝜏 ↔ (𝑓𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))
10 bnj1445.3 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐶 = {𝑓 ∣ ∃𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))}
11 nfre1 3303 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑑𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))
1211nfab 2981 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑑{𝑓 ∣ ∃𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))}
1310, 12nfcxfr 2972 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑑𝐶
1413nfcri 2968 . . . . . . . . . . . . . . . . . . . . . . 23 𝑑 𝑓𝐶
15 nfv 1906 . . . . . . . . . . . . . . . . . . . . . . 23 𝑑dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))
1614, 15nfan 1891 . . . . . . . . . . . . . . . . . . . . . 22 𝑑(𝑓𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))
179, 16nfxfr 1844 . . . . . . . . . . . . . . . . . . . . 21 𝑑𝜏
1817nfex 2334 . . . . . . . . . . . . . . . . . . . 20 𝑑𝑓𝜏
1918nfn 1848 . . . . . . . . . . . . . . . . . . 19 𝑑 ¬ ∃𝑓𝜏
20 nfcv 2974 . . . . . . . . . . . . . . . . . . 19 𝑑𝐴
2119, 20nfrabw 3383 . . . . . . . . . . . . . . . . . 18 𝑑{𝑥𝐴 ∣ ¬ ∃𝑓𝜏}
228, 21nfcxfr 2972 . . . . . . . . . . . . . . . . 17 𝑑𝐷
23 nfcv 2974 . . . . . . . . . . . . . . . . 17 𝑑
2422, 23nfne 3116 . . . . . . . . . . . . . . . 16 𝑑 𝐷 ≠ ∅
257, 24nfan 1891 . . . . . . . . . . . . . . 15 𝑑(𝑅 FrSe 𝐴𝐷 ≠ ∅)
266, 25nfxfr 1844 . . . . . . . . . . . . . 14 𝑑𝜓
2722nfcri 2968 . . . . . . . . . . . . . 14 𝑑 𝑥𝐷
28 nfv 1906 . . . . . . . . . . . . . . 15 𝑑 ¬ 𝑦𝑅𝑥
2922, 28nfralw 3222 . . . . . . . . . . . . . 14 𝑑𝑦𝐷 ¬ 𝑦𝑅𝑥
3026, 27, 29nf3an 1893 . . . . . . . . . . . . 13 𝑑(𝜓𝑥𝐷 ∧ ∀𝑦𝐷 ¬ 𝑦𝑅𝑥)
315, 30nfxfr 1844 . . . . . . . . . . . 12 𝑑𝜒
3231nf5ri 2185 . . . . . . . . . . 11 (𝜒 → ∀𝑑𝜒)
3332bnj1351 31997 . . . . . . . . . 10 ((𝜒𝑧𝐸) → ∀𝑑(𝜒𝑧𝐸))
3433nf5i 2141 . . . . . . . . 9 𝑑(𝜒𝑧𝐸)
354, 34nfxfr 1844 . . . . . . . 8 𝑑𝜃
36 nfv 1906 . . . . . . . 8 𝑑 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅)
3735, 36nfan 1891 . . . . . . 7 𝑑(𝜃𝑧 ∈ trCl(𝑥, 𝐴, 𝑅))
383, 37nfxfr 1844 . . . . . 6 𝑑𝜁
39 bnj1445.9 . . . . . . . 8 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}
40 nfcv 2974 . . . . . . . . . 10 𝑑 pred(𝑥, 𝐴, 𝑅)
41 bnj1445.8 . . . . . . . . . . 11 (𝜏′[𝑦 / 𝑥]𝜏)
42 nfcv 2974 . . . . . . . . . . . 12 𝑑𝑦
4342, 17nfsbcw 3791 . . . . . . . . . . 11 𝑑[𝑦 / 𝑥]𝜏
4441, 43nfxfr 1844 . . . . . . . . . 10 𝑑𝜏′
4540, 44nfrex 3306 . . . . . . . . 9 𝑑𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′
4645nfab 2981 . . . . . . . 8 𝑑{𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}
4739, 46nfcxfr 2972 . . . . . . 7 𝑑𝐻
4847nfcri 2968 . . . . . 6 𝑑 𝑓𝐻
49 nfv 1906 . . . . . 6 𝑑 𝑧 ∈ dom 𝑓
5038, 48, 49nf3an 1893 . . . . 5 𝑑(𝜁𝑓𝐻𝑧 ∈ dom 𝑓)
512, 50nfxfr 1844 . . . 4 𝑑𝜌
5251nf5ri 2185 . . 3 (𝜌 → ∀𝑑𝜌)
53 ax-5 1902 . . 3 (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) → ∀𝑑 𝑦 ∈ pred(𝑥, 𝐴, 𝑅))
5414nf5ri 2185 . . 3 (𝑓𝐶 → ∀𝑑 𝑓𝐶)
55 ax-5 1902 . . 3 (dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)) → ∀𝑑dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)))
5652, 53, 54, 55bnj982 31949 . 2 ((𝜌𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))) → ∀𝑑(𝜌𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))))
571, 56hbxfrbi 1816 1 (𝜎 → ∀𝑑𝜎)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079  wal 1526   = wceq 1528  wex 1771  wcel 2105  {cab 2796  wne 3013  wral 3135  wrex 3136  {crab 3139  [wsbc 3769  cun 3931  wss 3933  c0 4288  {csn 4557  cop 4563   cuni 4830   class class class wbr 5057  dom cdm 5548  cres 5550   Fn wfn 6343  cfv 6348  w-bnj17 31855   predc-bnj14 31857   FrSe w-bnj15 31861   trClc-bnj18 31863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-sbc 3770  df-bnj17 31856
This theorem is referenced by:  bnj1450  32219
  Copyright terms: Public domain W3C validator