Metamath Proof Explorer

Theorem isf32lem8

Description: Lemma for isfin3-2 . K sets are subsets of the base. (Contributed by Stefan O'Rear, 6-Nov-2014)

Ref Expression
Hypotheses isf32lem.a ${⊢}{\phi }\to {F}:\mathrm{\omega }⟶𝒫{G}$
isf32lem.b ${⊢}{\phi }\to \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left(\mathrm{suc}{x}\right)\subseteq {F}\left({x}\right)$
isf32lem.c ${⊢}{\phi }\to ¬\bigcap \mathrm{ran}{F}\in \mathrm{ran}{F}$
isf32lem.d ${⊢}{S}=\left\{{y}\in \mathrm{\omega }|{F}\left(\mathrm{suc}{y}\right)\subset {F}\left({y}\right)\right\}$
isf32lem.e ${⊢}{J}=\left({u}\in \mathrm{\omega }⟼\left(\iota {v}\in {S}|\left({v}\cap {S}\right)\approx {u}\right)\right)$
isf32lem.f ${⊢}{K}=\left({w}\in {S}⟼{F}\left({w}\right)\setminus {F}\left(\mathrm{suc}{w}\right)\right)\circ {J}$
Assertion isf32lem8 ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to {K}\left({A}\right)\subseteq {G}$

Proof

Step Hyp Ref Expression
1 isf32lem.a ${⊢}{\phi }\to {F}:\mathrm{\omega }⟶𝒫{G}$
2 isf32lem.b ${⊢}{\phi }\to \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{F}\left(\mathrm{suc}{x}\right)\subseteq {F}\left({x}\right)$
3 isf32lem.c ${⊢}{\phi }\to ¬\bigcap \mathrm{ran}{F}\in \mathrm{ran}{F}$
4 isf32lem.d ${⊢}{S}=\left\{{y}\in \mathrm{\omega }|{F}\left(\mathrm{suc}{y}\right)\subset {F}\left({y}\right)\right\}$
5 isf32lem.e ${⊢}{J}=\left({u}\in \mathrm{\omega }⟼\left(\iota {v}\in {S}|\left({v}\cap {S}\right)\approx {u}\right)\right)$
6 isf32lem.f ${⊢}{K}=\left({w}\in {S}⟼{F}\left({w}\right)\setminus {F}\left(\mathrm{suc}{w}\right)\right)\circ {J}$
7 6 fveq1i ${⊢}{K}\left({A}\right)=\left(\left({w}\in {S}⟼{F}\left({w}\right)\setminus {F}\left(\mathrm{suc}{w}\right)\right)\circ {J}\right)\left({A}\right)$
8 4 ssrab3 ${⊢}{S}\subseteq \mathrm{\omega }$
9 1 2 3 4 isf32lem5 ${⊢}{\phi }\to ¬{S}\in \mathrm{Fin}$
10 5 fin23lem22 ${⊢}\left({S}\subseteq \mathrm{\omega }\wedge ¬{S}\in \mathrm{Fin}\right)\to {J}:\mathrm{\omega }\underset{1-1 onto}{⟶}{S}$
11 8 9 10 sylancr ${⊢}{\phi }\to {J}:\mathrm{\omega }\underset{1-1 onto}{⟶}{S}$
12 f1of ${⊢}{J}:\mathrm{\omega }\underset{1-1 onto}{⟶}{S}\to {J}:\mathrm{\omega }⟶{S}$
13 11 12 syl ${⊢}{\phi }\to {J}:\mathrm{\omega }⟶{S}$
14 fvco3 ${⊢}\left({J}:\mathrm{\omega }⟶{S}\wedge {A}\in \mathrm{\omega }\right)\to \left(\left({w}\in {S}⟼{F}\left({w}\right)\setminus {F}\left(\mathrm{suc}{w}\right)\right)\circ {J}\right)\left({A}\right)=\left({w}\in {S}⟼{F}\left({w}\right)\setminus {F}\left(\mathrm{suc}{w}\right)\right)\left({J}\left({A}\right)\right)$
15 13 14 sylan ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to \left(\left({w}\in {S}⟼{F}\left({w}\right)\setminus {F}\left(\mathrm{suc}{w}\right)\right)\circ {J}\right)\left({A}\right)=\left({w}\in {S}⟼{F}\left({w}\right)\setminus {F}\left(\mathrm{suc}{w}\right)\right)\left({J}\left({A}\right)\right)$
16 13 ffvelrnda ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to {J}\left({A}\right)\in {S}$
17 fveq2 ${⊢}{w}={J}\left({A}\right)\to {F}\left({w}\right)={F}\left({J}\left({A}\right)\right)$
18 suceq ${⊢}{w}={J}\left({A}\right)\to \mathrm{suc}{w}=\mathrm{suc}{J}\left({A}\right)$
19 18 fveq2d ${⊢}{w}={J}\left({A}\right)\to {F}\left(\mathrm{suc}{w}\right)={F}\left(\mathrm{suc}{J}\left({A}\right)\right)$
20 17 19 difeq12d ${⊢}{w}={J}\left({A}\right)\to {F}\left({w}\right)\setminus {F}\left(\mathrm{suc}{w}\right)={F}\left({J}\left({A}\right)\right)\setminus {F}\left(\mathrm{suc}{J}\left({A}\right)\right)$
21 eqid ${⊢}\left({w}\in {S}⟼{F}\left({w}\right)\setminus {F}\left(\mathrm{suc}{w}\right)\right)=\left({w}\in {S}⟼{F}\left({w}\right)\setminus {F}\left(\mathrm{suc}{w}\right)\right)$
22 fvex ${⊢}{F}\left({J}\left({A}\right)\right)\in \mathrm{V}$
23 22 difexi ${⊢}{F}\left({J}\left({A}\right)\right)\setminus {F}\left(\mathrm{suc}{J}\left({A}\right)\right)\in \mathrm{V}$
24 20 21 23 fvmpt ${⊢}{J}\left({A}\right)\in {S}\to \left({w}\in {S}⟼{F}\left({w}\right)\setminus {F}\left(\mathrm{suc}{w}\right)\right)\left({J}\left({A}\right)\right)={F}\left({J}\left({A}\right)\right)\setminus {F}\left(\mathrm{suc}{J}\left({A}\right)\right)$
25 16 24 syl ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to \left({w}\in {S}⟼{F}\left({w}\right)\setminus {F}\left(\mathrm{suc}{w}\right)\right)\left({J}\left({A}\right)\right)={F}\left({J}\left({A}\right)\right)\setminus {F}\left(\mathrm{suc}{J}\left({A}\right)\right)$
26 15 25 eqtrd ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to \left(\left({w}\in {S}⟼{F}\left({w}\right)\setminus {F}\left(\mathrm{suc}{w}\right)\right)\circ {J}\right)\left({A}\right)={F}\left({J}\left({A}\right)\right)\setminus {F}\left(\mathrm{suc}{J}\left({A}\right)\right)$
27 7 26 syl5eq ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to {K}\left({A}\right)={F}\left({J}\left({A}\right)\right)\setminus {F}\left(\mathrm{suc}{J}\left({A}\right)\right)$
28 1 adantr ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to {F}:\mathrm{\omega }⟶𝒫{G}$
29 8 16 sseldi ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to {J}\left({A}\right)\in \mathrm{\omega }$
30 28 29 ffvelrnd ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to {F}\left({J}\left({A}\right)\right)\in 𝒫{G}$
31 30 elpwid ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to {F}\left({J}\left({A}\right)\right)\subseteq {G}$
32 31 ssdifssd ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to {F}\left({J}\left({A}\right)\right)\setminus {F}\left(\mathrm{suc}{J}\left({A}\right)\right)\subseteq {G}$
33 27 32 eqsstrd ${⊢}\left({\phi }\wedge {A}\in \mathrm{\omega }\right)\to {K}\left({A}\right)\subseteq {G}$