Metamath Proof Explorer

Theorem bnj1312

Description: Technical lemma for bnj60 . 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.)

Ref Expression
Hypotheses bnj1312.1 ${⊢}{B}=\left\{{d}|\left({d}\subseteq {A}\wedge \forall {x}\in {d}\phantom{\rule{.4em}{0ex}}pred\left({x},{A},{R}\right)\subseteq {d}\right)\right\}$
bnj1312.2 ${⊢}{Y}=⟨{x},{{f}↾}_{pred\left({x},{A},{R}\right)}⟩$
bnj1312.3 ${⊢}{C}=\left\{{f}|\exists {d}\in {B}\phantom{\rule{.4em}{0ex}}\left({f}Fn{d}\wedge \forall {x}\in {d}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={G}\left({Y}\right)\right)\right\}$
bnj1312.4 ${⊢}{\tau }↔\left({f}\in {C}\wedge \mathrm{dom}{f}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)\right)$
bnj1312.5 ${⊢}{D}=\left\{{x}\in {A}|¬\exists {f}\phantom{\rule{.4em}{0ex}}{\tau }\right\}$
bnj1312.6 ${⊢}{\psi }↔\left({R}FrSe{A}\wedge {D}\ne \varnothing \right)$
bnj1312.7 ${⊢}{\chi }↔\left({\psi }\wedge {x}\in {D}\wedge \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\right)$
bnj1312.8 No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
bnj1312.9 No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
bnj1312.10 ${⊢}{P}=\bigcup {H}$
bnj1312.11 ${⊢}{Z}=⟨{x},{{P}↾}_{pred\left({x},{A},{R}\right)}⟩$
bnj1312.12 ${⊢}{Q}={P}\cup \left\{⟨{x},{G}\left({Z}\right)⟩\right\}$
bnj1312.13 ${⊢}{W}=⟨{z},{{Q}↾}_{pred\left({z},{A},{R}\right)}⟩$
bnj1312.14 ${⊢}{E}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)$
Assertion bnj1312 ${⊢}{R}FrSe{A}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {f}\in {C}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{f}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)$

Proof

Step Hyp Ref Expression
1 bnj1312.1 ${⊢}{B}=\left\{{d}|\left({d}\subseteq {A}\wedge \forall {x}\in {d}\phantom{\rule{.4em}{0ex}}pred\left({x},{A},{R}\right)\subseteq {d}\right)\right\}$
2 bnj1312.2 ${⊢}{Y}=⟨{x},{{f}↾}_{pred\left({x},{A},{R}\right)}⟩$
3 bnj1312.3 ${⊢}{C}=\left\{{f}|\exists {d}\in {B}\phantom{\rule{.4em}{0ex}}\left({f}Fn{d}\wedge \forall {x}\in {d}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)={G}\left({Y}\right)\right)\right\}$
4 bnj1312.4 ${⊢}{\tau }↔\left({f}\in {C}\wedge \mathrm{dom}{f}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)\right)$
5 bnj1312.5 ${⊢}{D}=\left\{{x}\in {A}|¬\exists {f}\phantom{\rule{.4em}{0ex}}{\tau }\right\}$
6 bnj1312.6 ${⊢}{\psi }↔\left({R}FrSe{A}\wedge {D}\ne \varnothing \right)$
7 bnj1312.7 ${⊢}{\chi }↔\left({\psi }\wedge {x}\in {D}\wedge \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\right)$
8 bnj1312.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1312.9 Could not format H = { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
10 bnj1312.10 ${⊢}{P}=\bigcup {H}$
11 bnj1312.11 ${⊢}{Z}=⟨{x},{{P}↾}_{pred\left({x},{A},{R}\right)}⟩$
12 bnj1312.12 ${⊢}{Q}={P}\cup \left\{⟨{x},{G}\left({Z}\right)⟩\right\}$
13 bnj1312.13 ${⊢}{W}=⟨{z},{{Q}↾}_{pred\left({z},{A},{R}\right)}⟩$
14 bnj1312.14 ${⊢}{E}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)$
15 6 simplbi ${⊢}{\psi }\to {R}FrSe{A}$
16 5 ssrab3 ${⊢}{D}\subseteq {A}$
17 16 a1i ${⊢}{\psi }\to {D}\subseteq {A}$
18 6 simprbi ${⊢}{\psi }\to {D}\ne \varnothing$
19 5 bnj1230 ${⊢}{w}\in {D}\to \forall {x}\phantom{\rule{.4em}{0ex}}{w}\in {D}$
20 19 bnj1228 ${⊢}\left({R}FrSe{A}\wedge {D}\subseteq {A}\wedge {D}\ne \varnothing \right)\to \exists {x}\in {D}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}$
21 15 17 18 20 syl3anc ${⊢}{\psi }\to \exists {x}\in {D}\phantom{\rule{.4em}{0ex}}\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}$
22 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{R}FrSe{A}$
23 19 nfcii ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{D}$
24 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\varnothing$
25 23 24 nfne ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{D}\ne \varnothing$
26 22 25 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({R}FrSe{A}\wedge {D}\ne \varnothing \right)$
27 6 26 nfxfr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
28 27 nf5ri ${⊢}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }$
29 21 7 28 bnj1521 ${⊢}{\psi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\chi }$
30 7 simp2bi ${⊢}{\chi }\to {x}\in {D}$
31 5 bnj1538 ${⊢}{x}\in {D}\to ¬\exists {f}\phantom{\rule{.4em}{0ex}}{\tau }$
32 1 2 3 4 5 6 7 8 9 10 11 12 bnj1489 ${⊢}{\chi }\to {Q}\in \mathrm{V}$
33 7 15 bnj835 ${⊢}{\chi }\to {R}FrSe{A}$
34 1 2 3 4 5 6 7 8 9 10 bnj1384 ${⊢}{R}FrSe{A}\to \mathrm{Fun}{P}$
35 33 34 syl ${⊢}{\chi }\to \mathrm{Fun}{P}$
36 1 2 3 4 5 6 7 8 9 10 bnj1415 ${⊢}{\chi }\to \mathrm{dom}{P}=trCl\left({x},{A},{R}\right)$
37 35 36 bnj1422 ${⊢}{\chi }\to {P}FntrCl\left({x},{A},{R}\right)$
38 1 2 3 4 5 6 7 8 9 10 11 12 36 bnj1416 ${⊢}{\chi }\to \mathrm{dom}{Q}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)$
39 1 2 3 4 5 6 7 8 9 10 11 12 35 38 36 bnj1421 ${⊢}{\chi }\to \mathrm{Fun}{Q}$
40 39 38 bnj1422 ${⊢}{\chi }\to {Q}Fn\left(\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)\right)$
41 1 2 3 4 5 6 7 8 9 10 11 12 13 14 37 40 bnj1423 ${⊢}{\chi }\to \forall {z}\in {E}\phantom{\rule{.4em}{0ex}}{Q}\left({z}\right)={G}\left({W}\right)$
42 14 fneq2i ${⊢}{Q}Fn{E}↔{Q}Fn\left(\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)\right)$
43 40 42 sylibr ${⊢}{\chi }\to {Q}Fn{E}$
44 1 2 3 4 5 6 7 8 9 10 11 12 13 14 bnj1452 ${⊢}{\chi }\to {E}\in {B}$
45 1 2 3 4 5 6 7 8 9 10 11 12 13 14 32 41 43 44 bnj1463 ${⊢}{\chi }\to {Q}\in {C}$
46 45 38 jca ${⊢}{\chi }\to \left({Q}\in {C}\wedge \mathrm{dom}{Q}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)\right)$
47 1 2 3 4 5 6 7 8 9 10 11 12 46 bnj1491 ${⊢}\left({\chi }\wedge {Q}\in \mathrm{V}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\in {C}\wedge \mathrm{dom}{f}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)\right)$
48 32 47 mpdan ${⊢}{\chi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\in {C}\wedge \mathrm{dom}{f}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)\right)$
49 48 4 bnj1198 ${⊢}{\chi }\to \exists {f}\phantom{\rule{.4em}{0ex}}{\tau }$
50 31 49 nsyl3 ${⊢}{\chi }\to ¬{x}\in {D}$
51 29 30 50 bnj1304 ${⊢}¬{\psi }$
52 6 51 bnj1541 ${⊢}{R}FrSe{A}\to {D}=\varnothing$
53 5 52 bnj1476 ${⊢}{R}FrSe{A}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}{\tau }$
54 4 exbii ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}{\tau }↔\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\in {C}\wedge \mathrm{dom}{f}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)\right)$
55 df-rex ${⊢}\exists {f}\in {C}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{f}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}\in {C}\wedge \mathrm{dom}{f}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)\right)$
56 54 55 bitr4i ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}{\tau }↔\exists {f}\in {C}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{f}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)$
57 56 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}{\tau }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {f}\in {C}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{f}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)$
58 53 57 sylib ${⊢}{R}FrSe{A}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {f}\in {C}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{f}=\left\{{x}\right\}\cup trCl\left({x},{A},{R}\right)$