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 G V F : ω 𝒫 G b ω F suc b F b ¬ ran F ran F ω * G

Proof

Step Hyp Ref Expression
1 simp1 F : ω 𝒫 G b ω F suc b F b ¬ ran F ran F F : ω 𝒫 G
2 suceq b = c suc b = suc c
3 2 fveq2d b = c F suc b = F suc c
4 fveq2 b = c F b = F c
5 3 4 sseq12d b = c F suc b F b F suc c F c
6 5 cbvralvw b ω F suc b F b c ω F suc c F c
7 6 biimpi b ω F suc b F b c ω F suc c F c
8 7 3ad2ant2 F : ω 𝒫 G b ω F suc b F b ¬ ran F ran F c ω F suc c F c
9 simp3 F : ω 𝒫 G b ω F suc b F b ¬ ran F ran F ¬ ran F ran F
10 suceq e = d suc e = suc d
11 10 fveq2d e = d F suc e = F suc d
12 fveq2 e = d F e = F d
13 11 12 psseq12d e = d F suc e F e F suc d F d
14 13 cbvrabv e ω | F suc e F e = d ω | F suc d F d
15 eqid f ω ι g e ω | F suc e F e | g e ω | F suc e F e f = f ω ι g e ω | F suc e F e | g e ω | F suc e F e f
16 eqid h e ω | F suc e F e F h F suc h f ω ι g e ω | F suc e F e | g e ω | F suc e F e f = h e ω | F suc e F e F h F suc h f ω ι g e ω | F suc e F e | g e ω | F suc e F e f
17 eqid k G ι l | l ω k h e ω | F suc e F e F h F suc h f ω ι g e ω | F suc e F e | g e ω | F suc e F e f l = k G ι l | l ω k h e ω | F suc e F e F h F suc h f ω ι g e ω | F suc e F e | g e ω | F suc e F e f l
18 1 8 9 14 15 16 17 isf32lem10 F : ω 𝒫 G b ω F suc b F b ¬ ran F ran F G V ω * G
19 18 impcom G V F : ω 𝒫 G b ω F suc b F b ¬ ran F ran F ω * G