Metamath Proof Explorer


Theorem ttukeylem5

Description: Lemma for ttukey . The G function forms a (transfinitely long) chain of inclusions. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Hypotheses ttukeylem.1 φF:cardAB1-1 ontoAB
ttukeylem.2 φBA
ttukeylem.3 φxxA𝒫xFinA
ttukeylem.4 G=recszVifdomz=domzifdomz=BranzzdomzifzdomzFdomzAFdomz
Assertion ttukeylem5 φCOnDOnCDGCGD

Proof

Step Hyp Ref Expression
1 ttukeylem.1 φF:cardAB1-1 ontoAB
2 ttukeylem.2 φBA
3 ttukeylem.3 φxxA𝒫xFinA
4 ttukeylem.4 G=recszVifdomz=domzifdomz=BranzzdomzifzdomzFdomzAFdomz
5 sseq2 y=aCyCa
6 fveq2 y=aGy=Ga
7 6 sseq2d y=aGCGyGCGa
8 5 7 imbi12d y=aCyGCGyCaGCGa
9 8 imbi2d y=aφCOnCyGCGyφCOnCaGCGa
10 sseq2 y=DCyCD
11 fveq2 y=DGy=GD
12 11 sseq2d y=DGCGyGCGD
13 10 12 imbi12d y=DCyGCGyCDGCGD
14 13 imbi2d y=DφCOnCyGCGyφCOnCDGCGD
15 r19.21v ayφCOnCaGCGaφCOnayCaGCGa
16 onsseleq COnyOnCyCyC=y
17 16 ad4ant23 φCOnyOnayCaGCGaCyCyC=y
18 sseq2 ify=BGy=ify=yify=BGyGyifGyFyAFyGCify=BGyGCify=yify=BGyGyifGyFyAFy
19 sseq2 GyifGyFyAFy=ify=yify=BGyGyifGyFyAFyGCGyifGyFyAFyGCify=yify=BGyGyifGyFyAFy
20 4 tfr1 GFnOn
21 simplr φCOnyOnayCaGCGaCyyOn
22 onss yOnyOn
23 21 22 syl φCOnyOnayCaGCGaCyyOn
24 simprr φCOnyOnayCaGCGaCyCy
25 fnfvima GFnOnyOnCyGCGy
26 20 23 24 25 mp3an2i φCOnyOnayCaGCGaCyGCGy
27 elssuni GCGyGCGy
28 26 27 syl φCOnyOnayCaGCGaCyGCGy
29 n0i Cy¬y=
30 iffalse ¬y=ify=BGy=Gy
31 24 29 30 3syl φCOnyOnayCaGCGaCyify=BGy=Gy
32 28 31 sseqtrrd φCOnyOnayCaGCGaCyGCify=BGy
33 32 adantr φCOnyOnayCaGCGaCyy=yGCify=BGy
34 24 adantr φCOnyOnayCaGCGaCy¬y=yCy
35 elssuni CyCy
36 34 35 syl φCOnyOnayCaGCGaCy¬y=yCy
37 sseq2 a=yCaCy
38 fveq2 a=yGa=Gy
39 38 sseq2d a=yGCGaGCGy
40 37 39 imbi12d a=yCaGCGaCyGCGy
41 simplrl φCOnyOnayCaGCGaCy¬y=yayCaGCGa
42 vuniex yV
43 42 sucid ysucy
44 eloni yOnOrdy
45 orduniorsuc Ordyy=yy=sucy
46 21 44 45 3syl φCOnyOnayCaGCGaCyy=yy=sucy
47 46 orcanai φCOnyOnayCaGCGaCy¬y=yy=sucy
48 43 47 eleqtrrid φCOnyOnayCaGCGaCy¬y=yyy
49 40 41 48 rspcdva φCOnyOnayCaGCGaCy¬y=yCyGCGy
50 36 49 mpd φCOnyOnayCaGCGaCy¬y=yGCGy
51 ssun1 GyGyifGyFyAFy
52 50 51 sstrdi φCOnyOnayCaGCGaCy¬y=yGCGyifGyFyAFy
53 18 19 33 52 ifbothda φCOnyOnayCaGCGaCyGCify=yify=BGyGyifGyFyAFy
54 1 2 3 4 ttukeylem3 φyOnGy=ify=yify=BGyGyifGyFyAFy
55 54 ad4ant13 φCOnyOnayCaGCGaCyGy=ify=yify=BGyGyifGyFyAFy
56 53 55 sseqtrrd φCOnyOnayCaGCGaCyGCGy
57 56 expr φCOnyOnayCaGCGaCyGCGy
58 fveq2 C=yGC=Gy
59 eqimss GC=GyGCGy
60 58 59 syl C=yGCGy
61 60 a1i φCOnyOnayCaGCGaC=yGCGy
62 57 61 jaod φCOnyOnayCaGCGaCyC=yGCGy
63 17 62 sylbid φCOnyOnayCaGCGaCyGCGy
64 63 ex φCOnyOnayCaGCGaCyGCGy
65 64 expcom yOnφCOnayCaGCGaCyGCGy
66 65 a2d yOnφCOnayCaGCGaφCOnCyGCGy
67 15 66 syl5bi yOnayφCOnCaGCGaφCOnCyGCGy
68 9 14 67 tfis3 DOnφCOnCDGCGD
69 68 expdcom φCOnDOnCDGCGD
70 69 3imp2 φCOnDOnCDGCGD