Metamath Proof Explorer


Theorem erdszelem5

Description: Lemma for erdsze . (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypotheses erdsze.n φN
erdsze.f φF:1N1-1
erdszelem.k K=x1Nsup.y𝒫1x|FyIsom<,OyFyxy<
erdszelem.o OOr
Assertion erdszelem5 φA1NKA.y𝒫1A|FyIsom<,OyFyAy

Proof

Step Hyp Ref Expression
1 erdsze.n φN
2 erdsze.f φF:1N1-1
3 erdszelem.k K=x1Nsup.y𝒫1x|FyIsom<,OyFyxy<
4 erdszelem.o OOr
5 1 2 3 erdszelem3 A1NKA=sup.y𝒫1A|FyIsom<,OyFyAy<
6 5 adantl φA1NKA=sup.y𝒫1A|FyIsom<,OyFyAy<
7 snex AV
8 hashf .:V0+∞
9 8 fdmi dom.=V
10 7 9 eleqtrri Adom.
11 1 2 3 4 erdszelem4 φA1NAy𝒫1A|FyIsom<,OyFyAy
12 inelcm Adom.Ay𝒫1A|FyIsom<,OyFyAydom.y𝒫1A|FyIsom<,OyFyAy
13 10 11 12 sylancr φA1Ndom.y𝒫1A|FyIsom<,OyFyAy
14 imadisj .y𝒫1A|FyIsom<,OyFyAy=dom.y𝒫1A|FyIsom<,OyFyAy=
15 14 necon3bii .y𝒫1A|FyIsom<,OyFyAydom.y𝒫1A|FyIsom<,OyFyAy
16 13 15 sylibr φA1N.y𝒫1A|FyIsom<,OyFyAy
17 eqid y𝒫1A|FyIsom<,OyFyAy=y𝒫1A|FyIsom<,OyFyAy
18 17 erdszelem2 .y𝒫1A|FyIsom<,OyFyAyFin.y𝒫1A|FyIsom<,OyFyAy
19 18 simpli .y𝒫1A|FyIsom<,OyFyAyFin
20 18 simpri .y𝒫1A|FyIsom<,OyFyAy
21 nnssre
22 20 21 sstri .y𝒫1A|FyIsom<,OyFyAy
23 ltso <Or
24 fisupcl <Or.y𝒫1A|FyIsom<,OyFyAyFin.y𝒫1A|FyIsom<,OyFyAy.y𝒫1A|FyIsom<,OyFyAysup.y𝒫1A|FyIsom<,OyFyAy<.y𝒫1A|FyIsom<,OyFyAy
25 23 24 mpan .y𝒫1A|FyIsom<,OyFyAyFin.y𝒫1A|FyIsom<,OyFyAy.y𝒫1A|FyIsom<,OyFyAysup.y𝒫1A|FyIsom<,OyFyAy<.y𝒫1A|FyIsom<,OyFyAy
26 19 22 25 mp3an13 .y𝒫1A|FyIsom<,OyFyAysup.y𝒫1A|FyIsom<,OyFyAy<.y𝒫1A|FyIsom<,OyFyAy
27 16 26 syl φA1Nsup.y𝒫1A|FyIsom<,OyFyAy<.y𝒫1A|FyIsom<,OyFyAy
28 6 27 eqeltrd φA1NKA.y𝒫1A|FyIsom<,OyFyAy