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 32390
Description: Technical lemma for bnj60 32408. 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 1915 . . . . . . . . . . . . . . . 16 𝑑 𝑅 FrSe 𝐴
8 bnj1445.5 . . . . . . . . . . . . . . . . . 18 𝐷 = {𝑥𝐴 ∣ ¬ ∃𝑓𝜏}
9 bnj1445.4 . . . . . . . . . . . . . . . . . . . . . 22 (𝜏 ↔ (𝑓𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))
10 bnj1445.3 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐶 = {𝑓 ∣ ∃𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))}
11 nfre1 3292 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑑𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))
1211nfab 2985 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑑{𝑓 ∣ ∃𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))}
1310, 12nfcxfr 2977 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑑𝐶
1413nfcri 2967 . . . . . . . . . . . . . . . . . . . . . . 23 𝑑 𝑓𝐶
15 nfv 1915 . . . . . . . . . . . . . . . . . . . . . . 23 𝑑dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))
1614, 15nfan 1900 . . . . . . . . . . . . . . . . . . . . . 22 𝑑(𝑓𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))
179, 16nfxfr 1854 . . . . . . . . . . . . . . . . . . . . 21 𝑑𝜏
1817nfex 2344 . . . . . . . . . . . . . . . . . . . 20 𝑑𝑓𝜏
1918nfn 1858 . . . . . . . . . . . . . . . . . . 19 𝑑 ¬ ∃𝑓𝜏
20 nfcv 2979 . . . . . . . . . . . . . . . . . . 19 𝑑𝐴
2119, 20nfrabw 3366 . . . . . . . . . . . . . . . . . 18 𝑑{𝑥𝐴 ∣ ¬ ∃𝑓𝜏}
228, 21nfcxfr 2977 . . . . . . . . . . . . . . . . 17 𝑑𝐷
23 nfcv 2979 . . . . . . . . . . . . . . . . 17 𝑑
2422, 23nfne 3111 . . . . . . . . . . . . . . . 16 𝑑 𝐷 ≠ ∅
257, 24nfan 1900 . . . . . . . . . . . . . . 15 𝑑(𝑅 FrSe 𝐴𝐷 ≠ ∅)
266, 25nfxfr 1854 . . . . . . . . . . . . . 14 𝑑𝜓
2722nfcri 2967 . . . . . . . . . . . . . 14 𝑑 𝑥𝐷
28 nfv 1915 . . . . . . . . . . . . . . 15 𝑑 ¬ 𝑦𝑅𝑥
2922, 28nfralw 3214 . . . . . . . . . . . . . 14 𝑑𝑦𝐷 ¬ 𝑦𝑅𝑥
3026, 27, 29nf3an 1902 . . . . . . . . . . . . 13 𝑑(𝜓𝑥𝐷 ∧ ∀𝑦𝐷 ¬ 𝑦𝑅𝑥)
315, 30nfxfr 1854 . . . . . . . . . . . 12 𝑑𝜒
3231nf5ri 2196 . . . . . . . . . . 11 (𝜒 → ∀𝑑𝜒)
3332bnj1351 32172 . . . . . . . . . 10 ((𝜒𝑧𝐸) → ∀𝑑(𝜒𝑧𝐸))
3433nf5i 2150 . . . . . . . . 9 𝑑(𝜒𝑧𝐸)
354, 34nfxfr 1854 . . . . . . . 8 𝑑𝜃
36 nfv 1915 . . . . . . . 8 𝑑 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅)
3735, 36nfan 1900 . . . . . . 7 𝑑(𝜃𝑧 ∈ trCl(𝑥, 𝐴, 𝑅))
383, 37nfxfr 1854 . . . . . 6 𝑑𝜁
39 bnj1445.9 . . . . . . . 8 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}
40 nfcv 2979 . . . . . . . . . 10 𝑑 pred(𝑥, 𝐴, 𝑅)
41 bnj1445.8 . . . . . . . . . . 11 (𝜏′[𝑦 / 𝑥]𝜏)
42 nfcv 2979 . . . . . . . . . . . 12 𝑑𝑦
4342, 17nfsbcw 3769 . . . . . . . . . . 11 𝑑[𝑦 / 𝑥]𝜏
4441, 43nfxfr 1854 . . . . . . . . . 10 𝑑𝜏′
4540, 44nfrex 3295 . . . . . . . . 9 𝑑𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′
4645nfab 2985 . . . . . . . 8 𝑑{𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}
4739, 46nfcxfr 2977 . . . . . . 7 𝑑𝐻
4847nfcri 2967 . . . . . 6 𝑑 𝑓𝐻
49 nfv 1915 . . . . . 6 𝑑 𝑧 ∈ dom 𝑓
5038, 48, 49nf3an 1902 . . . . 5 𝑑(𝜁𝑓𝐻𝑧 ∈ dom 𝑓)
512, 50nfxfr 1854 . . . 4 𝑑𝜌
5251nf5ri 2196 . . 3 (𝜌 → ∀𝑑𝜌)
53 ax-5 1911 . . 3 (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) → ∀𝑑 𝑦 ∈ pred(𝑥, 𝐴, 𝑅))
5414nf5ri 2196 . . 3 (𝑓𝐶 → ∀𝑑 𝑓𝐶)
55 ax-5 1911 . . 3 (dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)) → ∀𝑑dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)))
5652, 53, 54, 55bnj982 32124 . 2 ((𝜌𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))) → ∀𝑑(𝜌𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))))
571, 56hbxfrbi 1826 1 (𝜎 → ∀𝑑𝜎)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084  wal 1536   = wceq 1538  wex 1781  wcel 2114  {cab 2800  wne 3011  wral 3130  wrex 3131  {crab 3134  [wsbc 3747  cun 3906  wss 3908  c0 4265  {csn 4539  cop 4545   cuni 4813   class class class wbr 5042  dom cdm 5532  cres 5534   Fn wfn 6329  cfv 6334  w-bnj17 32030   predc-bnj14 32032   FrSe w-bnj15 32036   trClc-bnj18 32038
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-rab 3139  df-sbc 3748  df-bnj17 32031
This theorem is referenced by:  bnj1450  32396
  Copyright terms: Public domain W3C validator