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 : 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
Assertion erdszelem5 φ A 1 N K A . y 𝒫 1 A | F y Isom < , O y F y A y

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 1 2 3 erdszelem3 A 1 N K A = sup . y 𝒫 1 A | F y Isom < , O y F y A y <
6 5 adantl φ A 1 N K A = sup . y 𝒫 1 A | F y Isom < , O y F y A y <
7 snex A V
8 hashf . : V 0 +∞
9 8 fdmi dom . = V
10 7 9 eleqtrri A dom .
11 1 2 3 4 erdszelem4 φ A 1 N A y 𝒫 1 A | F y Isom < , O y F y A y
12 inelcm A dom . A y 𝒫 1 A | F y Isom < , O y F y A y dom . y 𝒫 1 A | F y Isom < , O y F y A y
13 10 11 12 sylancr φ A 1 N dom . y 𝒫 1 A | F y Isom < , O y F y A y
14 imadisj . y 𝒫 1 A | F y Isom < , O y F y A y = dom . y 𝒫 1 A | F y Isom < , O y F y A y =
15 14 necon3bii . y 𝒫 1 A | F y Isom < , O y F y A y dom . y 𝒫 1 A | F y Isom < , O y F y A y
16 13 15 sylibr φ A 1 N . y 𝒫 1 A | F y Isom < , O y F y A y
17 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
18 17 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
19 18 simpli . y 𝒫 1 A | F y Isom < , O y F y A y Fin
20 18 simpri . y 𝒫 1 A | F y Isom < , O y F y A y
21 nnssre
22 20 21 sstri . y 𝒫 1 A | F y Isom < , O y F y A y
23 ltso < Or
24 fisupcl < Or . 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 . y 𝒫 1 A | F y Isom < , O y F y A y sup . y 𝒫 1 A | F y Isom < , O y F y A y < . y 𝒫 1 A | F y Isom < , O y F y A y
25 23 24 mpan . 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 . y 𝒫 1 A | F y Isom < , O y F y A y sup . y 𝒫 1 A | F y Isom < , O y F y A y < . y 𝒫 1 A | F y Isom < , O y F y A y
26 19 22 25 mp3an13 . y 𝒫 1 A | F y Isom < , O y F y A y sup . y 𝒫 1 A | F y Isom < , O y F y A y < . y 𝒫 1 A | F y Isom < , O y F y A y
27 16 26 syl φ A 1 N sup . y 𝒫 1 A | F y Isom < , O y F y A y < . y 𝒫 1 A | F y Isom < , O y F y A y
28 6 27 eqeltrd φ A 1 N K A . y 𝒫 1 A | F y Isom < , O y F y A y