Step | Hyp | Ref
| Expression |
1 | | erdsze2lem.n |
. . . . . . . . 9
⊢ 𝑁 = ((𝑅 − 1) · (𝑆 − 1)) |
2 | | erdsze2.r |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ ℕ) |
3 | | nnm1nn0 11334 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ ℕ → (𝑅 − 1) ∈
ℕ0) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 − 1) ∈
ℕ0) |
5 | | erdsze2.s |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ ℕ) |
6 | | nnm1nn0 11334 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ ℕ → (𝑆 − 1) ∈
ℕ0) |
7 | 5, 6 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 − 1) ∈
ℕ0) |
8 | 4, 7 | nn0mulcld 11356 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑅 − 1) · (𝑆 − 1)) ∈
ℕ0) |
9 | 1, 8 | syl5eqel 2705 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
10 | | peano2nn0 11333 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
11 | | hashfz1 13134 |
. . . . . . . 8
⊢ ((𝑁 + 1) ∈ ℕ0
→ (#‘(1...(𝑁 +
1))) = (𝑁 +
1)) |
12 | 9, 10, 11 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (#‘(1...(𝑁 + 1))) = (𝑁 + 1)) |
13 | 12 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ Fin) → (#‘(1...(𝑁 + 1))) = (𝑁 + 1)) |
14 | | erdsze2lem.l |
. . . . . . . 8
⊢ (𝜑 → 𝑁 < (#‘𝐴)) |
15 | 14 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ Fin) → 𝑁 < (#‘𝐴)) |
16 | | hashcl 13147 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin →
(#‘𝐴) ∈
ℕ0) |
17 | | nn0ltp1le 11435 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝐴) ∈
ℕ0) → (𝑁 < (#‘𝐴) ↔ (𝑁 + 1) ≤ (#‘𝐴))) |
18 | 9, 16, 17 | syl2an 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ Fin) → (𝑁 < (#‘𝐴) ↔ (𝑁 + 1) ≤ (#‘𝐴))) |
19 | 15, 18 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ Fin) → (𝑁 + 1) ≤ (#‘𝐴)) |
20 | 13, 19 | eqbrtrd 4675 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ Fin) → (#‘(1...(𝑁 + 1))) ≤ (#‘𝐴)) |
21 | | fzfid 12772 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ Fin) → (1...(𝑁 + 1)) ∈ Fin) |
22 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ∈ Fin) → 𝐴 ∈ Fin) |
23 | | hashdom 13168 |
. . . . . 6
⊢
(((1...(𝑁 + 1))
∈ Fin ∧ 𝐴 ∈
Fin) → ((#‘(1...(𝑁 + 1))) ≤ (#‘𝐴) ↔ (1...(𝑁 + 1)) ≼ 𝐴)) |
24 | 21, 22, 23 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ Fin) → ((#‘(1...(𝑁 + 1))) ≤ (#‘𝐴) ↔ (1...(𝑁 + 1)) ≼ 𝐴)) |
25 | 20, 24 | mpbid 222 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ Fin) → (1...(𝑁 + 1)) ≼ 𝐴) |
26 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ Fin) → ¬ 𝐴 ∈ Fin) |
27 | | fzfid 12772 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ Fin) → (1...(𝑁 + 1)) ∈ Fin) |
28 | | isinffi 8818 |
. . . . . 6
⊢ ((¬
𝐴 ∈ Fin ∧
(1...(𝑁 + 1)) ∈ Fin)
→ ∃𝑓 𝑓:(1...(𝑁 + 1))–1-1→𝐴) |
29 | 26, 27, 28 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ Fin) → ∃𝑓 𝑓:(1...(𝑁 + 1))–1-1→𝐴) |
30 | | erdsze2.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
31 | | reex 10027 |
. . . . . . . 8
⊢ ℝ
∈ V |
32 | | ssexg 4804 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ ℝ
∈ V) → 𝐴 ∈
V) |
33 | 30, 31, 32 | sylancl 694 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ V) |
34 | 33 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ Fin) → 𝐴 ∈ V) |
35 | | brdomg 7965 |
. . . . . 6
⊢ (𝐴 ∈ V → ((1...(𝑁 + 1)) ≼ 𝐴 ↔ ∃𝑓 𝑓:(1...(𝑁 + 1))–1-1→𝐴)) |
36 | 34, 35 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ Fin) → ((1...(𝑁 + 1)) ≼ 𝐴 ↔ ∃𝑓 𝑓:(1...(𝑁 + 1))–1-1→𝐴)) |
37 | 29, 36 | mpbird 247 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ Fin) → (1...(𝑁 + 1)) ≼ 𝐴) |
38 | 25, 37 | pm2.61dan 832 |
. . 3
⊢ (𝜑 → (1...(𝑁 + 1)) ≼ 𝐴) |
39 | | domeng 7969 |
. . . 4
⊢ (𝐴 ∈ V → ((1...(𝑁 + 1)) ≼ 𝐴 ↔ ∃𝑠((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴))) |
40 | 33, 39 | syl 17 |
. . 3
⊢ (𝜑 → ((1...(𝑁 + 1)) ≼ 𝐴 ↔ ∃𝑠((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴))) |
41 | 38, 40 | mpbid 222 |
. 2
⊢ (𝜑 → ∃𝑠((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) |
42 | | simprr 796 |
. . . . . 6
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → 𝑠 ⊆ 𝐴) |
43 | 30 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → 𝐴 ⊆ ℝ) |
44 | 42, 43 | sstrd 3613 |
. . . . 5
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → 𝑠 ⊆ ℝ) |
45 | | ltso 10118 |
. . . . 5
⊢ < Or
ℝ |
46 | | soss 5053 |
. . . . 5
⊢ (𝑠 ⊆ ℝ → ( <
Or ℝ → < Or 𝑠)) |
47 | 44, 45, 46 | mpisyl 21 |
. . . 4
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → < Or 𝑠) |
48 | | fzfid 12772 |
. . . . 5
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → (1...(𝑁 + 1)) ∈ Fin) |
49 | | simprl 794 |
. . . . . 6
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → (1...(𝑁 + 1)) ≈ 𝑠) |
50 | | enfi 8176 |
. . . . . 6
⊢
((1...(𝑁 + 1))
≈ 𝑠 →
((1...(𝑁 + 1)) ∈ Fin
↔ 𝑠 ∈
Fin)) |
51 | 49, 50 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → ((1...(𝑁 + 1)) ∈ Fin ↔ 𝑠 ∈ Fin)) |
52 | 48, 51 | mpbid 222 |
. . . 4
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → 𝑠 ∈ Fin) |
53 | | fz1iso 13246 |
. . . 4
⊢ (( <
Or 𝑠 ∧ 𝑠 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) |
54 | 47, 52, 53 | syl2anc 693 |
. . 3
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → ∃𝑓 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) |
55 | | isof1o 6573 |
. . . . . . . . . 10
⊢ (𝑓 Isom < , <
((1...(#‘𝑠)), 𝑠) → 𝑓:(1...(#‘𝑠))–1-1-onto→𝑠) |
56 | 55 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) ∧ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) → 𝑓:(1...(#‘𝑠))–1-1-onto→𝑠) |
57 | | hashen 13135 |
. . . . . . . . . . . . . . 15
⊢
(((1...(𝑁 + 1))
∈ Fin ∧ 𝑠 ∈
Fin) → ((#‘(1...(𝑁 + 1))) = (#‘𝑠) ↔ (1...(𝑁 + 1)) ≈ 𝑠)) |
58 | 48, 52, 57 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → ((#‘(1...(𝑁 + 1))) = (#‘𝑠) ↔ (1...(𝑁 + 1)) ≈ 𝑠)) |
59 | 49, 58 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → (#‘(1...(𝑁 + 1))) = (#‘𝑠)) |
60 | 12 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → (#‘(1...(𝑁 + 1))) = (𝑁 + 1)) |
61 | 59, 60 | eqtr3d 2658 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → (#‘𝑠) = (𝑁 + 1)) |
62 | 61 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) ∧ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) → (#‘𝑠) = (𝑁 + 1)) |
63 | 62 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) ∧ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) → (1...(#‘𝑠)) = (1...(𝑁 + 1))) |
64 | | f1oeq2 6128 |
. . . . . . . . . 10
⊢
((1...(#‘𝑠)) =
(1...(𝑁 + 1)) → (𝑓:(1...(#‘𝑠))–1-1-onto→𝑠 ↔ 𝑓:(1...(𝑁 + 1))–1-1-onto→𝑠)) |
65 | 63, 64 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) ∧ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) → (𝑓:(1...(#‘𝑠))–1-1-onto→𝑠 ↔ 𝑓:(1...(𝑁 + 1))–1-1-onto→𝑠)) |
66 | 56, 65 | mpbid 222 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) ∧ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) → 𝑓:(1...(𝑁 + 1))–1-1-onto→𝑠) |
67 | | f1of1 6136 |
. . . . . . . 8
⊢ (𝑓:(1...(𝑁 + 1))–1-1-onto→𝑠 → 𝑓:(1...(𝑁 + 1))–1-1→𝑠) |
68 | 66, 67 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) ∧ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) → 𝑓:(1...(𝑁 + 1))–1-1→𝑠) |
69 | | simplrr 801 |
. . . . . . 7
⊢ (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) ∧ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) → 𝑠 ⊆ 𝐴) |
70 | | f1ss 6106 |
. . . . . . 7
⊢ ((𝑓:(1...(𝑁 + 1))–1-1→𝑠 ∧ 𝑠 ⊆ 𝐴) → 𝑓:(1...(𝑁 + 1))–1-1→𝐴) |
71 | 68, 69, 70 | syl2anc 693 |
. . . . . 6
⊢ (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) ∧ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) → 𝑓:(1...(𝑁 + 1))–1-1→𝐴) |
72 | | simpr 477 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) ∧ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) → 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) |
73 | | f1ofo 6144 |
. . . . . . . . 9
⊢ (𝑓:(1...(#‘𝑠))–1-1-onto→𝑠 → 𝑓:(1...(#‘𝑠))–onto→𝑠) |
74 | | forn 6118 |
. . . . . . . . 9
⊢ (𝑓:(1...(#‘𝑠))–onto→𝑠 → ran 𝑓 = 𝑠) |
75 | | isoeq5 6571 |
. . . . . . . . 9
⊢ (ran
𝑓 = 𝑠 → (𝑓 Isom < , < ((1...(#‘𝑠)), ran 𝑓) ↔ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠))) |
76 | 56, 73, 74, 75 | 4syl 19 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) ∧ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) → (𝑓 Isom < , < ((1...(#‘𝑠)), ran 𝑓) ↔ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠))) |
77 | 72, 76 | mpbird 247 |
. . . . . . 7
⊢ (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) ∧ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) → 𝑓 Isom < , < ((1...(#‘𝑠)), ran 𝑓)) |
78 | | isoeq4 6570 |
. . . . . . . 8
⊢
((1...(#‘𝑠)) =
(1...(𝑁 + 1)) → (𝑓 Isom < , <
((1...(#‘𝑠)), ran
𝑓) ↔ 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓))) |
79 | 63, 78 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) ∧ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) → (𝑓 Isom < , < ((1...(#‘𝑠)), ran 𝑓) ↔ 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓))) |
80 | 77, 79 | mpbid 222 |
. . . . . 6
⊢ (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) ∧ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) → 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓)) |
81 | 71, 80 | jca 554 |
. . . . 5
⊢ (((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) ∧ 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠)) → (𝑓:(1...(𝑁 + 1))–1-1→𝐴 ∧ 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓))) |
82 | 81 | ex 450 |
. . . 4
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → (𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠) → (𝑓:(1...(𝑁 + 1))–1-1→𝐴 ∧ 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓)))) |
83 | 82 | eximdv 1846 |
. . 3
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → (∃𝑓 𝑓 Isom < , < ((1...(#‘𝑠)), 𝑠) → ∃𝑓(𝑓:(1...(𝑁 + 1))–1-1→𝐴 ∧ 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓)))) |
84 | 54, 83 | mpd 15 |
. 2
⊢ ((𝜑 ∧ ((1...(𝑁 + 1)) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴)) → ∃𝑓(𝑓:(1...(𝑁 + 1))–1-1→𝐴 ∧ 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓))) |
85 | 41, 84 | exlimddv 1863 |
1
⊢ (𝜑 → ∃𝑓(𝑓:(1...(𝑁 + 1))–1-1→𝐴 ∧ 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓))) |