Metamath Proof Explorer


Theorem fin23lem36

Description: Lemma for fin23 . Weak order property of Y . (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypotheses fin23lem33.f F=g|a𝒫gωxωasucxaxranarana
fin23lem.f φh:ω1-1V
fin23lem.g φranhG
fin23lem.h φjj:ω1-1VranjGij:ω1-1Vranijranj
fin23lem.i Y=recihω
Assertion fin23lem36 AωBωBAφranYAranYB

Proof

Step Hyp Ref Expression
1 fin23lem33.f F=g|a𝒫gωxωasucxaxranarana
2 fin23lem.f φh:ω1-1V
3 fin23lem.g φranhG
4 fin23lem.h φjj:ω1-1VranjGij:ω1-1Vranijranj
5 fin23lem.i Y=recihω
6 fveq2 a=BYa=YB
7 6 rneqd a=BranYa=ranYB
8 7 unieqd a=BranYa=ranYB
9 8 sseq1d a=BranYaranYBranYBranYB
10 9 imbi2d a=BφranYaranYBφranYBranYB
11 fveq2 a=bYa=Yb
12 11 rneqd a=branYa=ranYb
13 12 unieqd a=branYa=ranYb
14 13 sseq1d a=branYaranYBranYbranYB
15 14 imbi2d a=bφranYaranYBφranYbranYB
16 fveq2 a=sucbYa=Ysucb
17 16 rneqd a=sucbranYa=ranYsucb
18 17 unieqd a=sucbranYa=ranYsucb
19 18 sseq1d a=sucbranYaranYBranYsucbranYB
20 19 imbi2d a=sucbφranYaranYBφranYsucbranYB
21 fveq2 a=AYa=YA
22 21 rneqd a=AranYa=ranYA
23 22 unieqd a=AranYa=ranYA
24 23 sseq1d a=AranYaranYBranYAranYB
25 24 imbi2d a=AφranYaranYBφranYAranYB
26 ssid ranYBranYB
27 26 2a1i BωφranYBranYB
28 simprr bωBωBbφφ
29 simpll bωBωBbφbω
30 1 2 3 4 5 fin23lem35 φbωranYsucbranYb
31 28 29 30 syl2anc bωBωBbφranYsucbranYb
32 31 pssssd bωBωBbφranYsucbranYb
33 sstr2 ranYsucbranYbranYbranYBranYsucbranYB
34 32 33 syl bωBωBbφranYbranYBranYsucbranYB
35 34 expr bωBωBbφranYbranYBranYsucbranYB
36 35 a2d bωBωBbφranYbranYBφranYsucbranYB
37 10 15 20 25 27 36 findsg AωBωBAφranYAranYB
38 37 impr AωBωBAφranYAranYB