Metamath Proof Explorer


Theorem erdszelem11

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.i I = x 1 N sup . y 𝒫 1 x | F y Isom < , < y F y x y <
erdszelem.j J = x 1 N sup . y 𝒫 1 x | F y Isom < , < -1 y F y x y <
erdszelem.t T = n 1 N I n J n
erdszelem.r φ R
erdszelem.s φ S
erdszelem.m φ R 1 S 1 < N
Assertion erdszelem11 φ s 𝒫 1 N R s F s Isom < , < s F s S s F s Isom < , < -1 s F s

Proof

Step Hyp Ref Expression
1 erdsze.n φ N
2 erdsze.f φ F : 1 N 1-1
3 erdszelem.i I = x 1 N sup . y 𝒫 1 x | F y Isom < , < y F y x y <
4 erdszelem.j J = x 1 N sup . y 𝒫 1 x | F y Isom < , < -1 y F y x y <
5 erdszelem.t T = n 1 N I n J n
6 erdszelem.r φ R
7 erdszelem.s φ S
8 erdszelem.m φ R 1 S 1 < N
9 1 2 3 4 5 6 7 8 erdszelem10 φ m 1 N ¬ I m 1 R 1 ¬ J m 1 S 1
10 1 adantr φ m 1 N ¬ I m 1 R 1 N
11 2 adantr φ m 1 N ¬ I m 1 R 1 F : 1 N 1-1
12 ltso < Or
13 simprl φ m 1 N ¬ I m 1 R 1 m 1 N
14 6 adantr φ m 1 N ¬ I m 1 R 1 R
15 simprr φ m 1 N ¬ I m 1 R 1 ¬ I m 1 R 1
16 10 11 3 12 13 14 15 erdszelem7 φ m 1 N ¬ I m 1 R 1 s 𝒫 1 N R s F s Isom < , < s F s
17 16 expr φ m 1 N ¬ I m 1 R 1 s 𝒫 1 N R s F s Isom < , < s F s
18 1 adantr φ m 1 N ¬ J m 1 S 1 N
19 2 adantr φ m 1 N ¬ J m 1 S 1 F : 1 N 1-1
20 gtso < -1 Or
21 simprl φ m 1 N ¬ J m 1 S 1 m 1 N
22 7 adantr φ m 1 N ¬ J m 1 S 1 S
23 simprr φ m 1 N ¬ J m 1 S 1 ¬ J m 1 S 1
24 18 19 4 20 21 22 23 erdszelem7 φ m 1 N ¬ J m 1 S 1 s 𝒫 1 N S s F s Isom < , < -1 s F s
25 24 expr φ m 1 N ¬ J m 1 S 1 s 𝒫 1 N S s F s Isom < , < -1 s F s
26 17 25 orim12d φ m 1 N ¬ I m 1 R 1 ¬ J m 1 S 1 s 𝒫 1 N R s F s Isom < , < s F s s 𝒫 1 N S s F s Isom < , < -1 s F s
27 26 rexlimdva φ m 1 N ¬ I m 1 R 1 ¬ J m 1 S 1 s 𝒫 1 N R s F s Isom < , < s F s s 𝒫 1 N S s F s Isom < , < -1 s F s
28 9 27 mpd φ s 𝒫 1 N R s F s Isom < , < s F s s 𝒫 1 N S s F s Isom < , < -1 s F s
29 r19.43 s 𝒫 1 N R s F s Isom < , < s F s S s F s Isom < , < -1 s F s s 𝒫 1 N R s F s Isom < , < s F s s 𝒫 1 N S s F s Isom < , < -1 s F s
30 28 29 sylibr φ s 𝒫 1 N R s F s Isom < , < s F s S s F s Isom < , < -1 s F s