Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  erdsze2lem1 Structured version   Visualization version   GIF version

Theorem erdsze2lem1 31381
Description: Lemma for erdsze2 31383. (Contributed by Mario Carneiro, 22-Jan-2015.)
Hypotheses
Ref Expression
erdsze2.r (𝜑𝑅 ∈ ℕ)
erdsze2.s (𝜑𝑆 ∈ ℕ)
erdsze2.f (𝜑𝐹:𝐴1-1→ℝ)
erdsze2.a (𝜑𝐴 ⊆ ℝ)
erdsze2lem.n 𝑁 = ((𝑅 − 1) · (𝑆 − 1))
erdsze2lem.l (𝜑𝑁 < (♯‘𝐴))
Assertion
Ref Expression
erdsze2lem1 (𝜑 → ∃𝑓(𝑓:(1...(𝑁 + 1))–1-1𝐴𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓)))
Distinct variable groups:   𝐴,𝑓   𝑓,𝐹   𝑅,𝑓   𝑆,𝑓   𝑓,𝑁   𝜑,𝑓

Proof of Theorem erdsze2lem1
Dummy variable 𝑠 is distinct from all other variables.
StepHypRef Expression
1 erdsze2lem.n . . . . . . . . 9 𝑁 = ((𝑅 − 1) · (𝑆 − 1))
2 erdsze2.r . . . . . . . . . . 11 (𝜑𝑅 ∈ ℕ)
3 nnm1nn0 11415 . . . . . . . . . . 11 (𝑅 ∈ ℕ → (𝑅 − 1) ∈ ℕ0)
42, 3syl 17 . . . . . . . . . 10 (𝜑 → (𝑅 − 1) ∈ ℕ0)
5 erdsze2.s . . . . . . . . . . 11 (𝜑𝑆 ∈ ℕ)
6 nnm1nn0 11415 . . . . . . . . . . 11 (𝑆 ∈ ℕ → (𝑆 − 1) ∈ ℕ0)
75, 6syl 17 . . . . . . . . . 10 (𝜑 → (𝑆 − 1) ∈ ℕ0)
84, 7nn0mulcld 11437 . . . . . . . . 9 (𝜑 → ((𝑅 − 1) · (𝑆 − 1)) ∈ ℕ0)
91, 8syl5eqel 2775 . . . . . . . 8 (𝜑𝑁 ∈ ℕ0)
10 peano2nn0 11414 . . . . . . . 8 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
11 hashfz1 13217 . . . . . . . 8 ((𝑁 + 1) ∈ ℕ0 → (♯‘(1...(𝑁 + 1))) = (𝑁 + 1))
129, 10, 113syl 18 . . . . . . 7 (𝜑 → (♯‘(1...(𝑁 + 1))) = (𝑁 + 1))
1312adantr 472 . . . . . 6 ((𝜑𝐴 ∈ Fin) → (♯‘(1...(𝑁 + 1))) = (𝑁 + 1))
14 erdsze2lem.l . . . . . . . 8 (𝜑𝑁 < (♯‘𝐴))
1514adantr 472 . . . . . . 7 ((𝜑𝐴 ∈ Fin) → 𝑁 < (♯‘𝐴))
16 hashcl 13228 . . . . . . . 8 (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
17 nn0ltp1le 11516 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ0) → (𝑁 < (♯‘𝐴) ↔ (𝑁 + 1) ≤ (♯‘𝐴)))
189, 16, 17syl2an 495 . . . . . . 7 ((𝜑𝐴 ∈ Fin) → (𝑁 < (♯‘𝐴) ↔ (𝑁 + 1) ≤ (♯‘𝐴)))
1915, 18mpbid 222 . . . . . 6 ((𝜑𝐴 ∈ Fin) → (𝑁 + 1) ≤ (♯‘𝐴))
2013, 19eqbrtrd 4750 . . . . 5 ((𝜑𝐴 ∈ Fin) → (♯‘(1...(𝑁 + 1))) ≤ (♯‘𝐴))
21 fzfid 12855 . . . . . 6 ((𝜑𝐴 ∈ Fin) → (1...(𝑁 + 1)) ∈ Fin)
22 simpr 479 . . . . . 6 ((𝜑𝐴 ∈ Fin) → 𝐴 ∈ Fin)
23 hashdom 13249 . . . . . 6 (((1...(𝑁 + 1)) ∈ Fin ∧ 𝐴 ∈ Fin) → ((♯‘(1...(𝑁 + 1))) ≤ (♯‘𝐴) ↔ (1...(𝑁 + 1)) ≼ 𝐴))
2421, 22, 23syl2anc 696 . . . . 5 ((𝜑𝐴 ∈ Fin) → ((♯‘(1...(𝑁 + 1))) ≤ (♯‘𝐴) ↔ (1...(𝑁 + 1)) ≼ 𝐴))
2520, 24mpbid 222 . . . 4 ((𝜑𝐴 ∈ Fin) → (1...(𝑁 + 1)) ≼ 𝐴)
26 simpr 479 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 ∈ Fin) → ¬ 𝐴 ∈ Fin)
27 fzfid 12855 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 ∈ Fin) → (1...(𝑁 + 1)) ∈ Fin)
28 isinffi 8899 . . . . . 6 ((¬ 𝐴 ∈ Fin ∧ (1...(𝑁 + 1)) ∈ Fin) → ∃𝑓 𝑓:(1...(𝑁 + 1))–1-1𝐴)
2926, 27, 28syl2anc 696 . . . . 5 ((𝜑 ∧ ¬ 𝐴 ∈ Fin) → ∃𝑓 𝑓:(1...(𝑁 + 1))–1-1𝐴)
30 erdsze2.a . . . . . . . 8 (𝜑𝐴 ⊆ ℝ)
31 reex 10108 . . . . . . . 8 ℝ ∈ V
32 ssexg 4880 . . . . . . . 8 ((𝐴 ⊆ ℝ ∧ ℝ ∈ V) → 𝐴 ∈ V)
3330, 31, 32sylancl 697 . . . . . . 7 (𝜑𝐴 ∈ V)
3433adantr 472 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ∈ V)
35 brdomg 8050 . . . . . 6 (𝐴 ∈ V → ((1...(𝑁 + 1)) ≼ 𝐴 ↔ ∃𝑓 𝑓:(1...(𝑁 + 1))–1-1𝐴))
3634, 35syl 17 . . . . 5 ((𝜑 ∧ ¬ 𝐴 ∈ Fin) → ((1...(𝑁 + 1)) ≼ 𝐴 ↔ ∃𝑓 𝑓:(1...(𝑁 + 1))–1-1𝐴))
3729, 36mpbird 247 . . . 4 ((𝜑 ∧ ¬ 𝐴 ∈ Fin) → (1...(𝑁 + 1)) ≼ 𝐴)
3825, 37pm2.61dan 867 . . 3 (𝜑 → (1...(𝑁 + 1)) ≼ 𝐴)
39 domeng 8054 . . . 4 (𝐴 ∈ V → ((1...(𝑁 + 1)) ≼ 𝐴 ↔ ∃𝑠((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)))
4033, 39syl 17 . . 3 (𝜑 → ((1...(𝑁 + 1)) ≼ 𝐴 ↔ ∃𝑠((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)))
4138, 40mpbid 222 . 2 (𝜑 → ∃𝑠((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴))
42 simprr 813 . . . . . 6 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → 𝑠𝐴)
4330adantr 472 . . . . . 6 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → 𝐴 ⊆ ℝ)
4442, 43sstrd 3687 . . . . 5 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → 𝑠 ⊆ ℝ)
45 ltso 10199 . . . . 5 < Or ℝ
46 soss 5125 . . . . 5 (𝑠 ⊆ ℝ → ( < Or ℝ → < Or 𝑠))
4744, 45, 46mpisyl 21 . . . 4 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → < Or 𝑠)
48 fzfid 12855 . . . . 5 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → (1...(𝑁 + 1)) ∈ Fin)
49 simprl 811 . . . . . 6 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → (1...(𝑁 + 1)) ≈ 𝑠)
50 enfi 8260 . . . . . 6 ((1...(𝑁 + 1)) ≈ 𝑠 → ((1...(𝑁 + 1)) ∈ Fin ↔ 𝑠 ∈ Fin))
5149, 50syl 17 . . . . 5 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → ((1...(𝑁 + 1)) ∈ Fin ↔ 𝑠 ∈ Fin))
5248, 51mpbid 222 . . . 4 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → 𝑠 ∈ Fin)
53 fz1iso 13327 . . . 4 (( < Or 𝑠𝑠 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠))
5447, 52, 53syl2anc 696 . . 3 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠))
55 isof1o 6656 . . . . . . . . . 10 (𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠) → 𝑓:(1...(♯‘𝑠))–1-1-onto𝑠)
5655adantl 473 . . . . . . . . 9 (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) ∧ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)) → 𝑓:(1...(♯‘𝑠))–1-1-onto𝑠)
57 hashen 13218 . . . . . . . . . . . . . . 15 (((1...(𝑁 + 1)) ∈ Fin ∧ 𝑠 ∈ Fin) → ((♯‘(1...(𝑁 + 1))) = (♯‘𝑠) ↔ (1...(𝑁 + 1)) ≈ 𝑠))
5848, 52, 57syl2anc 696 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → ((♯‘(1...(𝑁 + 1))) = (♯‘𝑠) ↔ (1...(𝑁 + 1)) ≈ 𝑠))
5949, 58mpbird 247 . . . . . . . . . . . . 13 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → (♯‘(1...(𝑁 + 1))) = (♯‘𝑠))
6012adantr 472 . . . . . . . . . . . . 13 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → (♯‘(1...(𝑁 + 1))) = (𝑁 + 1))
6159, 60eqtr3d 2728 . . . . . . . . . . . 12 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → (♯‘𝑠) = (𝑁 + 1))
6261adantr 472 . . . . . . . . . . 11 (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) ∧ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)) → (♯‘𝑠) = (𝑁 + 1))
6362oveq2d 6749 . . . . . . . . . 10 (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) ∧ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)) → (1...(♯‘𝑠)) = (1...(𝑁 + 1)))
64 f1oeq2 6209 . . . . . . . . . 10 ((1...(♯‘𝑠)) = (1...(𝑁 + 1)) → (𝑓:(1...(♯‘𝑠))–1-1-onto𝑠𝑓:(1...(𝑁 + 1))–1-1-onto𝑠))
6563, 64syl 17 . . . . . . . . 9 (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) ∧ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)) → (𝑓:(1...(♯‘𝑠))–1-1-onto𝑠𝑓:(1...(𝑁 + 1))–1-1-onto𝑠))
6656, 65mpbid 222 . . . . . . . 8 (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) ∧ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)) → 𝑓:(1...(𝑁 + 1))–1-1-onto𝑠)
67 f1of1 6217 . . . . . . . 8 (𝑓:(1...(𝑁 + 1))–1-1-onto𝑠𝑓:(1...(𝑁 + 1))–1-1𝑠)
6866, 67syl 17 . . . . . . 7 (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) ∧ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)) → 𝑓:(1...(𝑁 + 1))–1-1𝑠)
69 simplrr 820 . . . . . . 7 (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) ∧ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)) → 𝑠𝐴)
70 f1ss 6187 . . . . . . 7 ((𝑓:(1...(𝑁 + 1))–1-1𝑠𝑠𝐴) → 𝑓:(1...(𝑁 + 1))–1-1𝐴)
7168, 69, 70syl2anc 696 . . . . . 6 (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) ∧ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)) → 𝑓:(1...(𝑁 + 1))–1-1𝐴)
72 simpr 479 . . . . . . . 8 (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) ∧ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)) → 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠))
73 f1ofo 6225 . . . . . . . . 9 (𝑓:(1...(♯‘𝑠))–1-1-onto𝑠𝑓:(1...(♯‘𝑠))–onto𝑠)
74 forn 6199 . . . . . . . . 9 (𝑓:(1...(♯‘𝑠))–onto𝑠 → ran 𝑓 = 𝑠)
75 isoeq5 6654 . . . . . . . . 9 (ran 𝑓 = 𝑠 → (𝑓 Isom < , < ((1...(♯‘𝑠)), ran 𝑓) ↔ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)))
7656, 73, 74, 754syl 19 . . . . . . . 8 (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) ∧ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)) → (𝑓 Isom < , < ((1...(♯‘𝑠)), ran 𝑓) ↔ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)))
7772, 76mpbird 247 . . . . . . 7 (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) ∧ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)) → 𝑓 Isom < , < ((1...(♯‘𝑠)), ran 𝑓))
78 isoeq4 6653 . . . . . . . 8 ((1...(♯‘𝑠)) = (1...(𝑁 + 1)) → (𝑓 Isom < , < ((1...(♯‘𝑠)), ran 𝑓) ↔ 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓)))
7963, 78syl 17 . . . . . . 7 (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) ∧ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)) → (𝑓 Isom < , < ((1...(♯‘𝑠)), ran 𝑓) ↔ 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓)))
8077, 79mpbid 222 . . . . . 6 (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) ∧ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)) → 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓))
8171, 80jca 555 . . . . 5 (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) ∧ 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠)) → (𝑓:(1...(𝑁 + 1))–1-1𝐴𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓)))
8281ex 449 . . . 4 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → (𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠) → (𝑓:(1...(𝑁 + 1))–1-1𝐴𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓))))
8382eximdv 1927 . . 3 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑠)), 𝑠) → ∃𝑓(𝑓:(1...(𝑁 + 1))–1-1𝐴𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓))))
8454, 83mpd 15 . 2 ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠𝑠𝐴)) → ∃𝑓(𝑓:(1...(𝑁 + 1))–1-1𝐴𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓)))
8541, 84exlimddv 1944 1 (𝜑 → ∃𝑓(𝑓:(1...(𝑁 + 1))–1-1𝐴𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1564  wex 1785  wcel 2071  Vcvv 3272  wss 3648   class class class wbr 4728   Or wor 5106  ran crn 5187  1-1wf1 5966  ontowfo 5967  1-1-ontowf1o 5968  cfv 5969   Isom wiso 5970  (class class class)co 6733  cen 8037  cdom 8038  Fincfn 8040  cr 10016  1c1 10018   + caddc 10020   · cmul 10022   < clt 10155  cle 10156  cmin 10347  cn 11101  0cn0 11373  ...cfz 12408  chash 13200
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1818  ax-5 1920  ax-6 1986  ax-7 2022  ax-8 2073  ax-9 2080  ax-10 2100  ax-11 2115  ax-12 2128  ax-13 2323  ax-ext 2672  ax-rep 4847  ax-sep 4857  ax-nul 4865  ax-pow 4916  ax-pr 4979  ax-un 7034  ax-cnex 10073  ax-resscn 10074  ax-1cn 10075  ax-icn 10076  ax-addcl 10077  ax-addrcl 10078  ax-mulcl 10079  ax-mulrcl 10080  ax-mulcom 10081  ax-addass 10082  ax-mulass 10083  ax-distr 10084  ax-i2m1 10085  ax-1ne0 10086  ax-1rid 10087  ax-rnegex 10088  ax-rrecex 10089  ax-cnre 10090  ax-pre-lttri 10091  ax-pre-lttrn 10092  ax-pre-ltadd 10093  ax-pre-mulgt0 10094
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1567  df-ex 1786  df-nf 1791  df-sb 1979  df-eu 2543  df-mo 2544  df-clab 2679  df-cleq 2685  df-clel 2688  df-nfc 2823  df-ne 2865  df-nel 2968  df-ral 2987  df-rex 2988  df-reu 2989  df-rmo 2990  df-rab 2991  df-v 3274  df-sbc 3510  df-csb 3608  df-dif 3651  df-un 3653  df-in 3655  df-ss 3662  df-pss 3664  df-nul 3992  df-if 4163  df-pw 4236  df-sn 4254  df-pr 4256  df-tp 4258  df-op 4260  df-uni 4513  df-int 4552  df-iun 4598  df-br 4729  df-opab 4789  df-mpt 4806  df-tr 4829  df-id 5096  df-eprel 5101  df-po 5107  df-so 5108  df-fr 5145  df-se 5146  df-we 5147  df-xp 5192  df-rel 5193  df-cnv 5194  df-co 5195  df-dm 5196  df-rn 5197  df-res 5198  df-ima 5199  df-pred 5761  df-ord 5807  df-on 5808  df-lim 5809  df-suc 5810  df-iota 5932  df-fun 5971  df-fn 5972  df-f 5973  df-f1 5974  df-fo 5975  df-f1o 5976  df-fv 5977  df-isom 5978  df-riota 6694  df-ov 6736  df-oprab 6737  df-mpt2 6738  df-om 7151  df-1st 7253  df-2nd 7254  df-wrecs 7495  df-recs 7556  df-rdg 7594  df-1o 7648  df-oadd 7652  df-er 7830  df-en 8041  df-dom 8042  df-sdom 8043  df-fin 8044  df-oi 8499  df-card 8846  df-pnf 10157  df-mnf 10158  df-xr 10159  df-ltxr 10160  df-le 10161  df-sub 10349  df-neg 10350  df-nn 11102  df-n0 11374  df-xnn0 11445  df-z 11459  df-uz 11769  df-fz 12409  df-hash 13201
This theorem is referenced by:  erdsze2  31383
  Copyright terms: Public domain W3C validator