Proof of Theorem subfacp1lem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | disj 4449 | . . . 4
⊢ ((𝐾 ∩ {1, 𝑀}) = ∅ ↔ ∀𝑥 ∈ 𝐾 ¬ 𝑥 ∈ {1, 𝑀}) | 
| 2 |  | eldifi 4130 | . . . . . . . . 9
⊢ (𝑥 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) → 𝑥 ∈ (2...(𝑁 + 1))) | 
| 3 |  | elfzle1 13568 | . . . . . . . . 9
⊢ (𝑥 ∈ (2...(𝑁 + 1)) → 2 ≤ 𝑥) | 
| 4 |  | 1lt2 12438 | . . . . . . . . . . . 12
⊢ 1 <
2 | 
| 5 |  | 1re 11262 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℝ | 
| 6 |  | 2re 12341 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℝ | 
| 7 | 5, 6 | ltnlei 11383 | . . . . . . . . . . . 12
⊢ (1 < 2
↔ ¬ 2 ≤ 1) | 
| 8 | 4, 7 | mpbi 230 | . . . . . . . . . . 11
⊢  ¬ 2
≤ 1 | 
| 9 |  | breq2 5146 | . . . . . . . . . . 11
⊢ (𝑥 = 1 → (2 ≤ 𝑥 ↔ 2 ≤
1)) | 
| 10 | 8, 9 | mtbiri 327 | . . . . . . . . . 10
⊢ (𝑥 = 1 → ¬ 2 ≤ 𝑥) | 
| 11 | 10 | necon2ai 2969 | . . . . . . . . 9
⊢ (2 ≤
𝑥 → 𝑥 ≠ 1) | 
| 12 | 2, 3, 11 | 3syl 18 | . . . . . . . 8
⊢ (𝑥 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) → 𝑥 ≠ 1) | 
| 13 |  | eldifsni 4789 | . . . . . . . 8
⊢ (𝑥 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) → 𝑥 ≠ 𝑀) | 
| 14 | 12, 13 | jca 511 | . . . . . . 7
⊢ (𝑥 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) → (𝑥 ≠ 1 ∧ 𝑥 ≠ 𝑀)) | 
| 15 |  | subfacp1lem1.k | . . . . . . 7
⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀}) | 
| 16 | 14, 15 | eleq2s 2858 | . . . . . 6
⊢ (𝑥 ∈ 𝐾 → (𝑥 ≠ 1 ∧ 𝑥 ≠ 𝑀)) | 
| 17 |  | neanior 3034 | . . . . . 6
⊢ ((𝑥 ≠ 1 ∧ 𝑥 ≠ 𝑀) ↔ ¬ (𝑥 = 1 ∨ 𝑥 = 𝑀)) | 
| 18 | 16, 17 | sylib 218 | . . . . 5
⊢ (𝑥 ∈ 𝐾 → ¬ (𝑥 = 1 ∨ 𝑥 = 𝑀)) | 
| 19 |  | vex 3483 | . . . . . 6
⊢ 𝑥 ∈ V | 
| 20 | 19 | elpr 4649 | . . . . 5
⊢ (𝑥 ∈ {1, 𝑀} ↔ (𝑥 = 1 ∨ 𝑥 = 𝑀)) | 
| 21 | 18, 20 | sylnibr 329 | . . . 4
⊢ (𝑥 ∈ 𝐾 → ¬ 𝑥 ∈ {1, 𝑀}) | 
| 22 | 1, 21 | mprgbir 3067 | . . 3
⊢ (𝐾 ∩ {1, 𝑀}) = ∅ | 
| 23 | 22 | a1i 11 | . 2
⊢ (𝜑 → (𝐾 ∩ {1, 𝑀}) = ∅) | 
| 24 |  | uncom 4157 | . . . 4
⊢ ({1}
∪ (𝐾 ∪ {𝑀})) = ((𝐾 ∪ {𝑀}) ∪ {1}) | 
| 25 |  | 1z 12649 | . . . . . 6
⊢ 1 ∈
ℤ | 
| 26 |  | fzsn 13607 | . . . . . 6
⊢ (1 ∈
ℤ → (1...1) = {1}) | 
| 27 | 25, 26 | ax-mp 5 | . . . . 5
⊢ (1...1) =
{1} | 
| 28 | 15 | uneq1i 4163 | . . . . . 6
⊢ (𝐾 ∪ {𝑀}) = (((2...(𝑁 + 1)) ∖ {𝑀}) ∪ {𝑀}) | 
| 29 |  | undif1 4475 | . . . . . 6
⊢
(((2...(𝑁 + 1))
∖ {𝑀}) ∪ {𝑀}) = ((2...(𝑁 + 1)) ∪ {𝑀}) | 
| 30 | 28, 29 | eqtr2i 2765 | . . . . 5
⊢
((2...(𝑁 + 1)) ∪
{𝑀}) = (𝐾 ∪ {𝑀}) | 
| 31 | 27, 30 | uneq12i 4165 | . . . 4
⊢ ((1...1)
∪ ((2...(𝑁 + 1)) ∪
{𝑀})) = ({1} ∪ (𝐾 ∪ {𝑀})) | 
| 32 |  | df-pr 4628 | . . . . . . 7
⊢ {1, 𝑀} = ({1} ∪ {𝑀}) | 
| 33 | 32 | equncomi 4159 | . . . . . 6
⊢ {1, 𝑀} = ({𝑀} ∪ {1}) | 
| 34 | 33 | uneq2i 4164 | . . . . 5
⊢ (𝐾 ∪ {1, 𝑀}) = (𝐾 ∪ ({𝑀} ∪ {1})) | 
| 35 |  | unass 4171 | . . . . 5
⊢ ((𝐾 ∪ {𝑀}) ∪ {1}) = (𝐾 ∪ ({𝑀} ∪ {1})) | 
| 36 | 34, 35 | eqtr4i 2767 | . . . 4
⊢ (𝐾 ∪ {1, 𝑀}) = ((𝐾 ∪ {𝑀}) ∪ {1}) | 
| 37 | 24, 31, 36 | 3eqtr4i 2774 | . . 3
⊢ ((1...1)
∪ ((2...(𝑁 + 1)) ∪
{𝑀})) = (𝐾 ∪ {1, 𝑀}) | 
| 38 |  | subfacp1lem1.m | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1))) | 
| 39 | 38 | snssd 4808 | . . . . . . 7
⊢ (𝜑 → {𝑀} ⊆ (2...(𝑁 + 1))) | 
| 40 |  | ssequn2 4188 | . . . . . . 7
⊢ ({𝑀} ⊆ (2...(𝑁 + 1)) ↔ ((2...(𝑁 + 1)) ∪ {𝑀}) = (2...(𝑁 + 1))) | 
| 41 | 39, 40 | sylib 218 | . . . . . 6
⊢ (𝜑 → ((2...(𝑁 + 1)) ∪ {𝑀}) = (2...(𝑁 + 1))) | 
| 42 |  | df-2 12330 | . . . . . . 7
⊢ 2 = (1 +
1) | 
| 43 | 42 | oveq1i 7442 | . . . . . 6
⊢
(2...(𝑁 + 1)) = ((1
+ 1)...(𝑁 +
1)) | 
| 44 | 41, 43 | eqtrdi 2792 | . . . . 5
⊢ (𝜑 → ((2...(𝑁 + 1)) ∪ {𝑀}) = ((1 + 1)...(𝑁 + 1))) | 
| 45 | 44 | uneq2d 4167 | . . . 4
⊢ (𝜑 → ((1...1) ∪
((2...(𝑁 + 1)) ∪ {𝑀})) = ((1...1) ∪ ((1 +
1)...(𝑁 +
1)))) | 
| 46 |  | subfacp1lem1.n | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 47 | 46 | peano2nnd 12284 | . . . . . 6
⊢ (𝜑 → (𝑁 + 1) ∈ ℕ) | 
| 48 |  | nnuz 12922 | . . . . . 6
⊢ ℕ =
(ℤ≥‘1) | 
| 49 | 47, 48 | eleqtrdi 2850 | . . . . 5
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘1)) | 
| 50 |  | eluzfz1 13572 | . . . . 5
⊢ ((𝑁 + 1) ∈
(ℤ≥‘1) → 1 ∈ (1...(𝑁 + 1))) | 
| 51 |  | fzsplit 13591 | . . . . 5
⊢ (1 ∈
(1...(𝑁 + 1)) →
(1...(𝑁 + 1)) = ((1...1)
∪ ((1 + 1)...(𝑁 +
1)))) | 
| 52 | 49, 50, 51 | 3syl 18 | . . . 4
⊢ (𝜑 → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1)))) | 
| 53 | 45, 52 | eqtr4d 2779 | . . 3
⊢ (𝜑 → ((1...1) ∪
((2...(𝑁 + 1)) ∪ {𝑀})) = (1...(𝑁 + 1))) | 
| 54 | 37, 53 | eqtr3id 2790 | . 2
⊢ (𝜑 → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1))) | 
| 55 | 42 | oveq2i 7443 | . . 3
⊢ ((𝑁 + 1) − 2) = ((𝑁 + 1) − (1 +
1)) | 
| 56 |  | fzfi 14014 | . . . . . . . . 9
⊢
(2...(𝑁 + 1)) ∈
Fin | 
| 57 |  | diffi 9216 | . . . . . . . . 9
⊢
((2...(𝑁 + 1))
∈ Fin → ((2...(𝑁
+ 1)) ∖ {𝑀}) ∈
Fin) | 
| 58 | 56, 57 | ax-mp 5 | . . . . . . . 8
⊢
((2...(𝑁 + 1))
∖ {𝑀}) ∈
Fin | 
| 59 | 15, 58 | eqeltri 2836 | . . . . . . 7
⊢ 𝐾 ∈ Fin | 
| 60 |  | prfi 9364 | . . . . . . 7
⊢ {1, 𝑀} ∈ Fin | 
| 61 |  | hashun 14422 | . . . . . . 7
⊢ ((𝐾 ∈ Fin ∧ {1, 𝑀} ∈ Fin ∧ (𝐾 ∩ {1, 𝑀}) = ∅) → (♯‘(𝐾 ∪ {1, 𝑀})) = ((♯‘𝐾) + (♯‘{1, 𝑀}))) | 
| 62 | 59, 60, 22, 61 | mp3an 1462 | . . . . . 6
⊢
(♯‘(𝐾
∪ {1, 𝑀})) =
((♯‘𝐾) +
(♯‘{1, 𝑀})) | 
| 63 | 54 | fveq2d 6909 | . . . . . 6
⊢ (𝜑 → (♯‘(𝐾 ∪ {1, 𝑀})) = (♯‘(1...(𝑁 + 1)))) | 
| 64 |  | neeq1 3002 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑀 → (𝑥 ≠ 1 ↔ 𝑀 ≠ 1)) | 
| 65 | 3, 11 | syl 17 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (2...(𝑁 + 1)) → 𝑥 ≠ 1) | 
| 66 | 64, 65 | vtoclga 3576 | . . . . . . . . . 10
⊢ (𝑀 ∈ (2...(𝑁 + 1)) → 𝑀 ≠ 1) | 
| 67 | 38, 66 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑀 ≠ 1) | 
| 68 | 67 | necomd 2995 | . . . . . . . 8
⊢ (𝜑 → 1 ≠ 𝑀) | 
| 69 |  | 1ex 11258 | . . . . . . . . 9
⊢ 1 ∈
V | 
| 70 |  | subfacp1lem1.x | . . . . . . . . 9
⊢ 𝑀 ∈ V | 
| 71 |  | hashprg 14435 | . . . . . . . . 9
⊢ ((1
∈ V ∧ 𝑀 ∈ V)
→ (1 ≠ 𝑀 ↔
(♯‘{1, 𝑀}) =
2)) | 
| 72 | 69, 70, 71 | mp2an 692 | . . . . . . . 8
⊢ (1 ≠
𝑀 ↔ (♯‘{1,
𝑀}) = 2) | 
| 73 | 68, 72 | sylib 218 | . . . . . . 7
⊢ (𝜑 → (♯‘{1, 𝑀}) = 2) | 
| 74 | 73 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → ((♯‘𝐾) + (♯‘{1, 𝑀})) = ((♯‘𝐾) + 2)) | 
| 75 | 62, 63, 74 | 3eqtr3a 2800 | . . . . 5
⊢ (𝜑 → (♯‘(1...(𝑁 + 1))) = ((♯‘𝐾) + 2)) | 
| 76 | 47 | nnnn0d 12589 | . . . . . 6
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) | 
| 77 |  | hashfz1 14386 | . . . . . 6
⊢ ((𝑁 + 1) ∈ ℕ0
→ (♯‘(1...(𝑁 + 1))) = (𝑁 + 1)) | 
| 78 | 76, 77 | syl 17 | . . . . 5
⊢ (𝜑 → (♯‘(1...(𝑁 + 1))) = (𝑁 + 1)) | 
| 79 | 75, 78 | eqtr3d 2778 | . . . 4
⊢ (𝜑 → ((♯‘𝐾) + 2) = (𝑁 + 1)) | 
| 80 | 47 | nncnd 12283 | . . . . 5
⊢ (𝜑 → (𝑁 + 1) ∈ ℂ) | 
| 81 |  | 2cnd 12345 | . . . . 5
⊢ (𝜑 → 2 ∈
ℂ) | 
| 82 |  | hashcl 14396 | . . . . . . . 8
⊢ (𝐾 ∈ Fin →
(♯‘𝐾) ∈
ℕ0) | 
| 83 | 59, 82 | ax-mp 5 | . . . . . . 7
⊢
(♯‘𝐾)
∈ ℕ0 | 
| 84 | 83 | nn0cni 12540 | . . . . . 6
⊢
(♯‘𝐾)
∈ ℂ | 
| 85 | 84 | a1i 11 | . . . . 5
⊢ (𝜑 → (♯‘𝐾) ∈
ℂ) | 
| 86 | 80, 81, 85 | subadd2d 11640 | . . . 4
⊢ (𝜑 → (((𝑁 + 1) − 2) = (♯‘𝐾) ↔ ((♯‘𝐾) + 2) = (𝑁 + 1))) | 
| 87 | 79, 86 | mpbird 257 | . . 3
⊢ (𝜑 → ((𝑁 + 1) − 2) = (♯‘𝐾)) | 
| 88 | 46 | nncnd 12283 | . . . 4
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 89 |  | 1cnd 11257 | . . . 4
⊢ (𝜑 → 1 ∈
ℂ) | 
| 90 | 88, 89, 89 | pnpcan2d 11659 | . . 3
⊢ (𝜑 → ((𝑁 + 1) − (1 + 1)) = (𝑁 − 1)) | 
| 91 | 55, 87, 90 | 3eqtr3a 2800 | . 2
⊢ (𝜑 → (♯‘𝐾) = (𝑁 − 1)) | 
| 92 | 23, 54, 91 | 3jca 1128 | 1
⊢ (𝜑 → ((𝐾 ∩ {1, 𝑀}) = ∅ ∧ (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) ∧ (♯‘𝐾) = (𝑁 − 1))) |