Metamath Proof Explorer


Theorem erdszelem10

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 erdszelem10 φ m 1 N ¬ I m 1 R 1 ¬ J m 1 S 1

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 fzfi 1 R 1 Fin
10 fzfi 1 S 1 Fin
11 xpfi 1 R 1 Fin 1 S 1 Fin 1 R 1 × 1 S 1 Fin
12 9 10 11 mp2an 1 R 1 × 1 S 1 Fin
13 ssdomg 1 R 1 × 1 S 1 Fin ran T 1 R 1 × 1 S 1 ran T 1 R 1 × 1 S 1
14 12 13 ax-mp ran T 1 R 1 × 1 S 1 ran T 1 R 1 × 1 S 1
15 domnsym ran T 1 R 1 × 1 S 1 ¬ 1 R 1 × 1 S 1 ran T
16 14 15 syl ran T 1 R 1 × 1 S 1 ¬ 1 R 1 × 1 S 1 ran T
17 hashxp 1 R 1 Fin 1 S 1 Fin 1 R 1 × 1 S 1 = 1 R 1 1 S 1
18 9 10 17 mp2an 1 R 1 × 1 S 1 = 1 R 1 1 S 1
19 nnm1nn0 R R 1 0
20 hashfz1 R 1 0 1 R 1 = R 1
21 6 19 20 3syl φ 1 R 1 = R 1
22 nnm1nn0 S S 1 0
23 hashfz1 S 1 0 1 S 1 = S 1
24 7 22 23 3syl φ 1 S 1 = S 1
25 21 24 oveq12d φ 1 R 1 1 S 1 = R 1 S 1
26 18 25 syl5eq φ 1 R 1 × 1 S 1 = R 1 S 1
27 1 nnnn0d φ N 0
28 hashfz1 N 0 1 N = N
29 27 28 syl φ 1 N = N
30 8 26 29 3brtr4d φ 1 R 1 × 1 S 1 < 1 N
31 fzfid φ 1 N Fin
32 hashsdom 1 R 1 × 1 S 1 Fin 1 N Fin 1 R 1 × 1 S 1 < 1 N 1 R 1 × 1 S 1 1 N
33 12 31 32 sylancr φ 1 R 1 × 1 S 1 < 1 N 1 R 1 × 1 S 1 1 N
34 30 33 mpbid φ 1 R 1 × 1 S 1 1 N
35 1 2 3 4 5 erdszelem9 φ T : 1 N 1-1 ×
36 f1f1orn T : 1 N 1-1 × T : 1 N 1-1 onto ran T
37 ovex 1 N V
38 37 f1oen T : 1 N 1-1 onto ran T 1 N ran T
39 35 36 38 3syl φ 1 N ran T
40 sdomentr 1 R 1 × 1 S 1 1 N 1 N ran T 1 R 1 × 1 S 1 ran T
41 34 39 40 syl2anc φ 1 R 1 × 1 S 1 ran T
42 16 41 nsyl3 φ ¬ ran T 1 R 1 × 1 S 1
43 nss ¬ ran T 1 R 1 × 1 S 1 s s ran T ¬ s 1 R 1 × 1 S 1
44 df-rex s ran T ¬ s 1 R 1 × 1 S 1 s s ran T ¬ s 1 R 1 × 1 S 1
45 43 44 bitr4i ¬ ran T 1 R 1 × 1 S 1 s ran T ¬ s 1 R 1 × 1 S 1
46 42 45 sylib φ s ran T ¬ s 1 R 1 × 1 S 1
47 f1fn T : 1 N 1-1 × T Fn 1 N
48 eleq1 s = T m s 1 R 1 × 1 S 1 T m 1 R 1 × 1 S 1
49 48 notbid s = T m ¬ s 1 R 1 × 1 S 1 ¬ T m 1 R 1 × 1 S 1
50 49 rexrn T Fn 1 N s ran T ¬ s 1 R 1 × 1 S 1 m 1 N ¬ T m 1 R 1 × 1 S 1
51 35 47 50 3syl φ s ran T ¬ s 1 R 1 × 1 S 1 m 1 N ¬ T m 1 R 1 × 1 S 1
52 46 51 mpbid φ m 1 N ¬ T m 1 R 1 × 1 S 1
53 fveq2 n = m I n = I m
54 fveq2 n = m J n = J m
55 53 54 opeq12d n = m I n J n = I m J m
56 opex I m J m V
57 55 5 56 fvmpt m 1 N T m = I m J m
58 57 adantl φ m 1 N T m = I m J m
59 58 eleq1d φ m 1 N T m 1 R 1 × 1 S 1 I m J m 1 R 1 × 1 S 1
60 opelxp I m J m 1 R 1 × 1 S 1 I m 1 R 1 J m 1 S 1
61 59 60 bitrdi φ m 1 N T m 1 R 1 × 1 S 1 I m 1 R 1 J m 1 S 1
62 61 notbid φ m 1 N ¬ T m 1 R 1 × 1 S 1 ¬ I m 1 R 1 J m 1 S 1
63 ianor ¬ I m 1 R 1 J m 1 S 1 ¬ I m 1 R 1 ¬ J m 1 S 1
64 62 63 bitrdi φ m 1 N ¬ T m 1 R 1 × 1 S 1 ¬ I m 1 R 1 ¬ J m 1 S 1
65 64 rexbidva φ m 1 N ¬ T m 1 R 1 × 1 S 1 m 1 N ¬ I m 1 R 1 ¬ J m 1 S 1
66 52 65 mpbid φ m 1 N ¬ I m 1 R 1 ¬ J m 1 S 1