Metamath Proof Explorer


Theorem isf32lem11

Description: Lemma for isfin3-2 . Remove hypotheses from isf32lem10 . (Contributed by Stefan O'Rear, 17-May-2015)

Ref Expression
Assertion isf32lem11 GVF:ω𝒫GbωFsucbFb¬ranFranFω*G

Proof

Step Hyp Ref Expression
1 simp1 F:ω𝒫GbωFsucbFb¬ranFranFF:ω𝒫G
2 suceq b=csucb=succ
3 2 fveq2d b=cFsucb=Fsucc
4 fveq2 b=cFb=Fc
5 3 4 sseq12d b=cFsucbFbFsuccFc
6 5 cbvralvw bωFsucbFbcωFsuccFc
7 6 biimpi bωFsucbFbcωFsuccFc
8 7 3ad2ant2 F:ω𝒫GbωFsucbFb¬ranFranFcωFsuccFc
9 simp3 F:ω𝒫GbωFsucbFb¬ranFranF¬ranFranF
10 suceq e=dsuce=sucd
11 10 fveq2d e=dFsuce=Fsucd
12 fveq2 e=dFe=Fd
13 11 12 psseq12d e=dFsuceFeFsucdFd
14 13 cbvrabv eω|FsuceFe=dω|FsucdFd
15 eqid fωιgeω|FsuceFe|geω|FsuceFef=fωιgeω|FsuceFe|geω|FsuceFef
16 eqid heω|FsuceFeFhFsuchfωιgeω|FsuceFe|geω|FsuceFef=heω|FsuceFeFhFsuchfωιgeω|FsuceFe|geω|FsuceFef
17 eqid kGιl|lωkheω|FsuceFeFhFsuchfωιgeω|FsuceFe|geω|FsuceFefl=kGιl|lωkheω|FsuceFeFhFsuchfωιgeω|FsuceFe|geω|FsuceFefl
18 1 8 9 14 15 16 17 isf32lem10 F:ω𝒫GbωFsucbFb¬ranFranFGVω*G
19 18 impcom GVF:ω𝒫GbωFsucbFb¬ranFranFω*G