Metamath Proof Explorer


Theorem erdszelem4

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 erdszelem4 φ A 1 N 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 elfznn A 1 N A
6 5 adantl φ A 1 N A
7 elfz1end A A 1 A
8 6 7 sylib φ A 1 N A 1 A
9 8 snssd φ A 1 N A 1 A
10 elsni x A x = A
11 elsni y A y = A
12 10 11 breqan12d x A y A x < y A < A
13 12 adantl φ A 1 N x A y A x < y A < A
14 fzssuz 1 N 1
15 uzssz 1
16 zssre
17 15 16 sstri 1
18 14 17 sstri 1 N
19 simpr φ A 1 N A 1 N
20 19 adantr φ A 1 N x A y A A 1 N
21 18 20 sseldi φ A 1 N x A y A A
22 21 ltnrd φ A 1 N x A y A ¬ A < A
23 22 pm2.21d φ A 1 N x A y A A < A F x O F y
24 13 23 sylbid φ A 1 N x A y A x < y F x O F y
25 24 ralrimivva φ A 1 N x A y A x < y F x O F y
26 f1f F : 1 N 1-1 F : 1 N
27 2 26 syl φ F : 1 N
28 27 adantr φ A 1 N F : 1 N
29 19 snssd φ A 1 N A 1 N
30 ltso < Or
31 soss 1 N < Or < Or 1 N
32 18 30 31 mp2 < Or 1 N
33 soisores < Or 1 N O Or F : 1 N A 1 N F A Isom < , O A F A x A y A x < y F x O F y
34 32 4 33 mpanl12 F : 1 N A 1 N F A Isom < , O A F A x A y A x < y F x O F y
35 28 29 34 syl2anc φ A 1 N F A Isom < , O A F A x A y A x < y F x O F y
36 25 35 mpbird φ A 1 N F A Isom < , O A F A
37 snidg A 1 N A A
38 37 adantl φ A 1 N A A
39 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
40 39 erdszelem1 A y 𝒫 1 A | F y Isom < , O y F y A y A 1 A F A Isom < , O A F A A A
41 9 36 38 40 syl3anbrc φ A 1 N A y 𝒫 1 A | F y Isom < , O y F y A y