# Metamath Proof Explorer

## Theorem fin23lem39

Description: Lemma for fin23 . Thus, we have that g could not have been in F after all. (Contributed by Stefan O'Rear, 4-Nov-2014)

Ref Expression
Hypotheses fin23lem33.f ${⊢}{F}=\left\{{g}|\forall {a}\in \left({𝒫{g}}^{\mathrm{\omega }}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{a}\left(\mathrm{suc}{x}\right)\subseteq {a}\left({x}\right)\to \bigcap \mathrm{ran}{a}\in \mathrm{ran}{a}\right)\right\}$
fin23lem.f ${⊢}{\phi }\to {h}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}$
fin23lem.g ${⊢}{\phi }\to \bigcup \mathrm{ran}{h}\subseteq {G}$
fin23lem.h ${⊢}{\phi }\to \forall {j}\phantom{\rule{.4em}{0ex}}\left(\left({j}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{j}\subseteq {G}\right)\to \left({i}\left({j}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({j}\right)\subset \bigcup \mathrm{ran}{j}\right)\right)$
fin23lem.i ${⊢}{Y}={\mathrm{rec}\left({i},{h}\right)↾}_{\mathrm{\omega }}$
Assertion fin23lem39 ${⊢}{\phi }\to ¬{G}\in {F}$

### Proof

Step Hyp Ref Expression
1 fin23lem33.f ${⊢}{F}=\left\{{g}|\forall {a}\in \left({𝒫{g}}^{\mathrm{\omega }}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{a}\left(\mathrm{suc}{x}\right)\subseteq {a}\left({x}\right)\to \bigcap \mathrm{ran}{a}\in \mathrm{ran}{a}\right)\right\}$
2 fin23lem.f ${⊢}{\phi }\to {h}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}$
3 fin23lem.g ${⊢}{\phi }\to \bigcup \mathrm{ran}{h}\subseteq {G}$
4 fin23lem.h ${⊢}{\phi }\to \forall {j}\phantom{\rule{.4em}{0ex}}\left(\left({j}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{j}\subseteq {G}\right)\to \left({i}\left({j}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{i}\left({j}\right)\subset \bigcup \mathrm{ran}{j}\right)\right)$
5 fin23lem.i ${⊢}{Y}={\mathrm{rec}\left({i},{h}\right)↾}_{\mathrm{\omega }}$
6 1 2 3 4 5 fin23lem38 ${⊢}{\phi }\to ¬\bigcap \mathrm{ran}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\in \mathrm{ran}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)$
7 1 2 3 4 5 fin23lem35 ${⊢}\left({\phi }\wedge {e}\in \mathrm{\omega }\right)\to \bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{e}\right)\subset \bigcup \mathrm{ran}{Y}\left({e}\right)$
8 7 pssssd ${⊢}\left({\phi }\wedge {e}\in \mathrm{\omega }\right)\to \bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{e}\right)\subseteq \bigcup \mathrm{ran}{Y}\left({e}\right)$
9 peano2 ${⊢}{e}\in \mathrm{\omega }\to \mathrm{suc}{e}\in \mathrm{\omega }$
10 fveq2 ${⊢}{c}=\mathrm{suc}{e}\to {Y}\left({c}\right)={Y}\left(\mathrm{suc}{e}\right)$
11 10 rneqd ${⊢}{c}=\mathrm{suc}{e}\to \mathrm{ran}{Y}\left({c}\right)=\mathrm{ran}{Y}\left(\mathrm{suc}{e}\right)$
12 11 unieqd ${⊢}{c}=\mathrm{suc}{e}\to \bigcup \mathrm{ran}{Y}\left({c}\right)=\bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{e}\right)$
13 eqid ${⊢}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)=\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)$
14 fvex ${⊢}{Y}\left(\mathrm{suc}{e}\right)\in \mathrm{V}$
15 14 rnex ${⊢}\mathrm{ran}{Y}\left(\mathrm{suc}{e}\right)\in \mathrm{V}$
16 15 uniex ${⊢}\bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{e}\right)\in \mathrm{V}$
17 12 13 16 fvmpt ${⊢}\mathrm{suc}{e}\in \mathrm{\omega }\to \left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left(\mathrm{suc}{e}\right)=\bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{e}\right)$
18 9 17 syl ${⊢}{e}\in \mathrm{\omega }\to \left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left(\mathrm{suc}{e}\right)=\bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{e}\right)$
19 fveq2 ${⊢}{c}={e}\to {Y}\left({c}\right)={Y}\left({e}\right)$
20 19 rneqd ${⊢}{c}={e}\to \mathrm{ran}{Y}\left({c}\right)=\mathrm{ran}{Y}\left({e}\right)$
21 20 unieqd ${⊢}{c}={e}\to \bigcup \mathrm{ran}{Y}\left({c}\right)=\bigcup \mathrm{ran}{Y}\left({e}\right)$
22 fvex ${⊢}{Y}\left({e}\right)\in \mathrm{V}$
23 22 rnex ${⊢}\mathrm{ran}{Y}\left({e}\right)\in \mathrm{V}$
24 23 uniex ${⊢}\bigcup \mathrm{ran}{Y}\left({e}\right)\in \mathrm{V}$
25 21 13 24 fvmpt ${⊢}{e}\in \mathrm{\omega }\to \left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left({e}\right)=\bigcup \mathrm{ran}{Y}\left({e}\right)$
26 18 25 sseq12d ${⊢}{e}\in \mathrm{\omega }\to \left(\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left(\mathrm{suc}{e}\right)\subseteq \left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left({e}\right)↔\bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{e}\right)\subseteq \bigcup \mathrm{ran}{Y}\left({e}\right)\right)$
27 26 adantl ${⊢}\left({\phi }\wedge {e}\in \mathrm{\omega }\right)\to \left(\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left(\mathrm{suc}{e}\right)\subseteq \left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left({e}\right)↔\bigcup \mathrm{ran}{Y}\left(\mathrm{suc}{e}\right)\subseteq \bigcup \mathrm{ran}{Y}\left({e}\right)\right)$
28 8 27 mpbird ${⊢}\left({\phi }\wedge {e}\in \mathrm{\omega }\right)\to \left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left(\mathrm{suc}{e}\right)\subseteq \left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left({e}\right)$
29 28 ralrimiva ${⊢}{\phi }\to \forall {e}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left(\mathrm{suc}{e}\right)\subseteq \left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left({e}\right)$
30 29 adantr ${⊢}\left({\phi }\wedge {G}\in {F}\right)\to \forall {e}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left(\mathrm{suc}{e}\right)\subseteq \left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left({e}\right)$
31 fveq1 ${⊢}{d}=\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\to {d}\left(\mathrm{suc}{e}\right)=\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left(\mathrm{suc}{e}\right)$
32 fveq1 ${⊢}{d}=\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\to {d}\left({e}\right)=\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left({e}\right)$
33 31 32 sseq12d ${⊢}{d}=\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\to \left({d}\left(\mathrm{suc}{e}\right)\subseteq {d}\left({e}\right)↔\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left(\mathrm{suc}{e}\right)\subseteq \left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left({e}\right)\right)$
34 33 ralbidv ${⊢}{d}=\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\to \left(\forall {e}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{d}\left(\mathrm{suc}{e}\right)\subseteq {d}\left({e}\right)↔\forall {e}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left(\mathrm{suc}{e}\right)\subseteq \left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left({e}\right)\right)$
35 rneq ${⊢}{d}=\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\to \mathrm{ran}{d}=\mathrm{ran}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)$
36 35 inteqd ${⊢}{d}=\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\to \bigcap \mathrm{ran}{d}=\bigcap \mathrm{ran}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)$
37 36 35 eleq12d ${⊢}{d}=\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\to \left(\bigcap \mathrm{ran}{d}\in \mathrm{ran}{d}↔\bigcap \mathrm{ran}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\in \mathrm{ran}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\right)$
38 34 37 imbi12d ${⊢}{d}=\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\to \left(\left(\forall {e}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{d}\left(\mathrm{suc}{e}\right)\subseteq {d}\left({e}\right)\to \bigcap \mathrm{ran}{d}\in \mathrm{ran}{d}\right)↔\left(\forall {e}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left(\mathrm{suc}{e}\right)\subseteq \left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left({e}\right)\to \bigcap \mathrm{ran}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\in \mathrm{ran}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\right)\right)$
39 1 isfin3ds ${⊢}{G}\in {F}\to \left({G}\in {F}↔\forall {d}\in \left({𝒫{G}}^{\mathrm{\omega }}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {e}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{d}\left(\mathrm{suc}{e}\right)\subseteq {d}\left({e}\right)\to \bigcap \mathrm{ran}{d}\in \mathrm{ran}{d}\right)\right)$
40 39 ibi ${⊢}{G}\in {F}\to \forall {d}\in \left({𝒫{G}}^{\mathrm{\omega }}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {e}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{d}\left(\mathrm{suc}{e}\right)\subseteq {d}\left({e}\right)\to \bigcap \mathrm{ran}{d}\in \mathrm{ran}{d}\right)$
41 40 adantl ${⊢}\left({\phi }\wedge {G}\in {F}\right)\to \forall {d}\in \left({𝒫{G}}^{\mathrm{\omega }}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {e}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{d}\left(\mathrm{suc}{e}\right)\subseteq {d}\left({e}\right)\to \bigcap \mathrm{ran}{d}\in \mathrm{ran}{d}\right)$
42 1 2 3 4 5 fin23lem34 ${⊢}\left({\phi }\wedge {c}\in \mathrm{\omega }\right)\to \left({Y}\left({c}\right):\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\wedge \bigcup \mathrm{ran}{Y}\left({c}\right)\subseteq {G}\right)$
43 42 simprd ${⊢}\left({\phi }\wedge {c}\in \mathrm{\omega }\right)\to \bigcup \mathrm{ran}{Y}\left({c}\right)\subseteq {G}$
44 43 adantlr ${⊢}\left(\left({\phi }\wedge {G}\in {F}\right)\wedge {c}\in \mathrm{\omega }\right)\to \bigcup \mathrm{ran}{Y}\left({c}\right)\subseteq {G}$
45 elpw2g ${⊢}{G}\in {F}\to \left(\bigcup \mathrm{ran}{Y}\left({c}\right)\in 𝒫{G}↔\bigcup \mathrm{ran}{Y}\left({c}\right)\subseteq {G}\right)$
46 45 ad2antlr ${⊢}\left(\left({\phi }\wedge {G}\in {F}\right)\wedge {c}\in \mathrm{\omega }\right)\to \left(\bigcup \mathrm{ran}{Y}\left({c}\right)\in 𝒫{G}↔\bigcup \mathrm{ran}{Y}\left({c}\right)\subseteq {G}\right)$
47 44 46 mpbird ${⊢}\left(\left({\phi }\wedge {G}\in {F}\right)\wedge {c}\in \mathrm{\omega }\right)\to \bigcup \mathrm{ran}{Y}\left({c}\right)\in 𝒫{G}$
48 47 fmpttd ${⊢}\left({\phi }\wedge {G}\in {F}\right)\to \left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right):\mathrm{\omega }⟶𝒫{G}$
49 pwexg ${⊢}{G}\in {F}\to 𝒫{G}\in \mathrm{V}$
50 vex ${⊢}{h}\in \mathrm{V}$
51 f1f ${⊢}{h}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\to {h}:\mathrm{\omega }⟶\mathrm{V}$
52 dmfex ${⊢}\left({h}\in \mathrm{V}\wedge {h}:\mathrm{\omega }⟶\mathrm{V}\right)\to \mathrm{\omega }\in \mathrm{V}$
53 50 51 52 sylancr ${⊢}{h}:\mathrm{\omega }\underset{1-1}{⟶}\mathrm{V}\to \mathrm{\omega }\in \mathrm{V}$
54 2 53 syl ${⊢}{\phi }\to \mathrm{\omega }\in \mathrm{V}$
55 elmapg ${⊢}\left(𝒫{G}\in \mathrm{V}\wedge \mathrm{\omega }\in \mathrm{V}\right)\to \left(\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\in \left({𝒫{G}}^{\mathrm{\omega }}\right)↔\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right):\mathrm{\omega }⟶𝒫{G}\right)$
56 49 54 55 syl2anr ${⊢}\left({\phi }\wedge {G}\in {F}\right)\to \left(\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\in \left({𝒫{G}}^{\mathrm{\omega }}\right)↔\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right):\mathrm{\omega }⟶𝒫{G}\right)$
57 48 56 mpbird ${⊢}\left({\phi }\wedge {G}\in {F}\right)\to \left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\in \left({𝒫{G}}^{\mathrm{\omega }}\right)$
58 38 41 57 rspcdva ${⊢}\left({\phi }\wedge {G}\in {F}\right)\to \left(\forall {e}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left(\mathrm{suc}{e}\right)\subseteq \left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\left({e}\right)\to \bigcap \mathrm{ran}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\in \mathrm{ran}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\right)$
59 30 58 mpd ${⊢}\left({\phi }\wedge {G}\in {F}\right)\to \bigcap \mathrm{ran}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)\in \mathrm{ran}\left({c}\in \mathrm{\omega }⟼\bigcup \mathrm{ran}{Y}\left({c}\right)\right)$
60 6 59 mtand ${⊢}{\phi }\to ¬{G}\in {F}$