Metamath Proof Explorer


Theorem erdszelem7

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

Ref Expression
Hypotheses erdsze.n φ N
erdsze.f φ F : 1 N 1-1
erdszelem.k K = x 1 N sup . y 𝒫 1 x | F y Isom < , O y F y x y <
erdszelem.o O Or
erdszelem.a φ A 1 N
erdszelem7.r φ R
erdszelem7.m φ ¬ K A 1 R 1
Assertion erdszelem7 φ s 𝒫 1 N R s F s Isom < , O s F s

Proof

Step Hyp Ref Expression
1 erdsze.n φ N
2 erdsze.f φ F : 1 N 1-1
3 erdszelem.k K = x 1 N sup . y 𝒫 1 x | F y Isom < , O y F y x y <
4 erdszelem.o O Or
5 erdszelem.a φ A 1 N
6 erdszelem7.r φ R
7 erdszelem7.m φ ¬ K A 1 R 1
8 hashf . : V 0 +∞
9 ffun . : V 0 +∞ Fun .
10 8 9 ax-mp Fun .
11 1 2 3 4 erdszelem5 φ A 1 N K A . y 𝒫 1 A | F y Isom < , O y F y A y
12 5 11 mpdan φ K A . y 𝒫 1 A | F y Isom < , O y F y A y
13 fvelima Fun . K A . y 𝒫 1 A | F y Isom < , O y F y A y s y 𝒫 1 A | F y Isom < , O y F y A y s = K A
14 10 12 13 sylancr φ s y 𝒫 1 A | F y Isom < , O y F y A y s = K A
15 eqid y 𝒫 1 A | F y Isom < , O y F y A y = y 𝒫 1 A | F y Isom < , O y F y A y
16 15 erdszelem1 s y 𝒫 1 A | F y Isom < , O y F y A y s 1 A F s Isom < , O s F s A s
17 simprl1 φ s 1 A F s Isom < , O s F s A s s = K A s 1 A
18 elfzuz3 A 1 N N A
19 fzss2 N A 1 A 1 N
20 5 18 19 3syl φ 1 A 1 N
21 20 adantr φ s 1 A F s Isom < , O s F s A s s = K A 1 A 1 N
22 17 21 sstrd φ s 1 A F s Isom < , O s F s A s s = K A s 1 N
23 velpw s 𝒫 1 N s 1 N
24 22 23 sylibr φ s 1 A F s Isom < , O s F s A s s = K A s 𝒫 1 N
25 1 2 3 4 erdszelem6 φ K : 1 N
26 25 5 ffvelrnd φ K A
27 nnuz = 1
28 26 27 eleqtrdi φ K A 1
29 nnz R R
30 peano2zm R R 1
31 6 29 30 3syl φ R 1
32 elfz5 K A 1 R 1 K A 1 R 1 K A R 1
33 28 31 32 syl2anc φ K A 1 R 1 K A R 1
34 nnltlem1 K A R K A < R K A R 1
35 26 6 34 syl2anc φ K A < R K A R 1
36 33 35 bitr4d φ K A 1 R 1 K A < R
37 7 36 mtbid φ ¬ K A < R
38 6 nnred φ R
39 15 erdszelem2 . y 𝒫 1 A | F y Isom < , O y F y A y Fin . y 𝒫 1 A | F y Isom < , O y F y A y
40 39 simpri . y 𝒫 1 A | F y Isom < , O y F y A y
41 nnssre
42 40 41 sstri . y 𝒫 1 A | F y Isom < , O y F y A y
43 42 12 sseldi φ K A
44 38 43 lenltd φ R K A ¬ K A < R
45 37 44 mpbird φ R K A
46 45 adantr φ s 1 A F s Isom < , O s F s A s s = K A R K A
47 simprr φ s 1 A F s Isom < , O s F s A s s = K A s = K A
48 46 47 breqtrrd φ s 1 A F s Isom < , O s F s A s s = K A R s
49 simprl2 φ s 1 A F s Isom < , O s F s A s s = K A F s Isom < , O s F s
50 24 48 49 jca32 φ s 1 A F s Isom < , O s F s A s s = K A s 𝒫 1 N R s F s Isom < , O s F s
51 50 expr φ s 1 A F s Isom < , O s F s A s s = K A s 𝒫 1 N R s F s Isom < , O s F s
52 16 51 sylan2b φ s y 𝒫 1 A | F y Isom < , O y F y A y s = K A s 𝒫 1 N R s F s Isom < , O s F s
53 52 expimpd φ s y 𝒫 1 A | F y Isom < , O y F y A y s = K A s 𝒫 1 N R s F s Isom < , O s F s
54 53 reximdv2 φ s y 𝒫 1 A | F y Isom < , O y F y A y s = K A s 𝒫 1 N R s F s Isom < , O s F s
55 14 54 mpd φ s 𝒫 1 N R s F s Isom < , O s F s