Proof of Theorem rabren3dioph
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | vex 3484 | . . . . 5
⊢ 𝑏 ∈ V | 
| 2 |  | tpex 7766 | . . . . 5
⊢ {〈1,
𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉} ∈
V | 
| 3 | 1, 2 | coex 7952 | . . . 4
⊢ (𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}) ∈
V | 
| 4 |  | 1ne2 12474 | . . . . . . . . . 10
⊢ 1 ≠
2 | 
| 5 |  | 1re 11261 | . . . . . . . . . . 11
⊢ 1 ∈
ℝ | 
| 6 |  | 1lt3 12439 | . . . . . . . . . . 11
⊢ 1 <
3 | 
| 7 | 5, 6 | ltneii 11374 | . . . . . . . . . 10
⊢ 1 ≠
3 | 
| 8 |  | 2re 12340 | . . . . . . . . . . 11
⊢ 2 ∈
ℝ | 
| 9 |  | 2lt3 12438 | . . . . . . . . . . 11
⊢ 2 <
3 | 
| 10 | 8, 9 | ltneii 11374 | . . . . . . . . . 10
⊢ 2 ≠
3 | 
| 11 |  | 1ex 11257 | . . . . . . . . . . 11
⊢ 1 ∈
V | 
| 12 |  | 2ex 12343 | . . . . . . . . . . 11
⊢ 2 ∈
V | 
| 13 |  | 3ex 12348 | . . . . . . . . . . 11
⊢ 3 ∈
V | 
| 14 |  | rabren3dioph.b | . . . . . . . . . . . 12
⊢ 𝑋 ∈ (1...𝑁) | 
| 15 | 14 | elexi 3503 | . . . . . . . . . . 11
⊢ 𝑋 ∈ V | 
| 16 |  | rabren3dioph.c | . . . . . . . . . . . 12
⊢ 𝑌 ∈ (1...𝑁) | 
| 17 | 16 | elexi 3503 | . . . . . . . . . . 11
⊢ 𝑌 ∈ V | 
| 18 |  | rabren3dioph.d | . . . . . . . . . . . 12
⊢ 𝑍 ∈ (1...𝑁) | 
| 19 | 18 | elexi 3503 | . . . . . . . . . . 11
⊢ 𝑍 ∈ V | 
| 20 | 11, 12, 13, 15, 17, 19 | fntp 6627 | . . . . . . . . . 10
⊢ ((1 ≠
2 ∧ 1 ≠ 3 ∧ 2 ≠ 3) → {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉} Fn {1, 2, 3}) | 
| 21 | 4, 7, 10, 20 | mp3an 1463 | . . . . . . . . 9
⊢ {〈1,
𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉} Fn {1, 2,
3} | 
| 22 | 11 | tpid1 4768 | . . . . . . . . 9
⊢ 1 ∈
{1, 2, 3} | 
| 23 |  | fvco2 7006 | . . . . . . . . 9
⊢
(({〈1, 𝑋〉,
〈2, 𝑌〉, 〈3,
𝑍〉} Fn {1, 2, 3} ∧
1 ∈ {1, 2, 3}) → ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘1) = (𝑏‘({〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}‘1))) | 
| 24 | 21, 22, 23 | mp2an 692 | . . . . . . . 8
⊢ ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘1) = (𝑏‘({〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}‘1)) | 
| 25 | 11, 15 | fvtp1 7215 | . . . . . . . . . 10
⊢ ((1 ≠
2 ∧ 1 ≠ 3) → ({〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}‘1) = 𝑋) | 
| 26 | 4, 7, 25 | mp2an 692 | . . . . . . . . 9
⊢
({〈1, 𝑋〉,
〈2, 𝑌〉, 〈3,
𝑍〉}‘1) = 𝑋 | 
| 27 | 26 | fveq2i 6909 | . . . . . . . 8
⊢ (𝑏‘({〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}‘1)) = (𝑏‘𝑋) | 
| 28 | 24, 27 | eqtri 2765 | . . . . . . 7
⊢ ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘1) = (𝑏‘𝑋) | 
| 29 | 12 | tpid2 4770 | . . . . . . . . 9
⊢ 2 ∈
{1, 2, 3} | 
| 30 |  | fvco2 7006 | . . . . . . . . 9
⊢
(({〈1, 𝑋〉,
〈2, 𝑌〉, 〈3,
𝑍〉} Fn {1, 2, 3} ∧
2 ∈ {1, 2, 3}) → ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘2) = (𝑏‘({〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}‘2))) | 
| 31 | 21, 29, 30 | mp2an 692 | . . . . . . . 8
⊢ ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘2) = (𝑏‘({〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}‘2)) | 
| 32 | 12, 17 | fvtp2 7216 | . . . . . . . . . 10
⊢ ((1 ≠
2 ∧ 2 ≠ 3) → ({〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}‘2) = 𝑌) | 
| 33 | 4, 10, 32 | mp2an 692 | . . . . . . . . 9
⊢
({〈1, 𝑋〉,
〈2, 𝑌〉, 〈3,
𝑍〉}‘2) = 𝑌 | 
| 34 | 33 | fveq2i 6909 | . . . . . . . 8
⊢ (𝑏‘({〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}‘2)) = (𝑏‘𝑌) | 
| 35 | 31, 34 | eqtri 2765 | . . . . . . 7
⊢ ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘2) = (𝑏‘𝑌) | 
| 36 | 13 | tpid3 4773 | . . . . . . . . 9
⊢ 3 ∈
{1, 2, 3} | 
| 37 |  | fvco2 7006 | . . . . . . . . 9
⊢
(({〈1, 𝑋〉,
〈2, 𝑌〉, 〈3,
𝑍〉} Fn {1, 2, 3} ∧
3 ∈ {1, 2, 3}) → ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘3) = (𝑏‘({〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}‘3))) | 
| 38 | 21, 36, 37 | mp2an 692 | . . . . . . . 8
⊢ ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘3) = (𝑏‘({〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}‘3)) | 
| 39 | 13, 19 | fvtp3 7217 | . . . . . . . . . 10
⊢ ((1 ≠
3 ∧ 2 ≠ 3) → ({〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}‘3) = 𝑍) | 
| 40 | 7, 10, 39 | mp2an 692 | . . . . . . . . 9
⊢
({〈1, 𝑋〉,
〈2, 𝑌〉, 〈3,
𝑍〉}‘3) = 𝑍 | 
| 41 | 40 | fveq2i 6909 | . . . . . . . 8
⊢ (𝑏‘({〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}‘3)) = (𝑏‘𝑍) | 
| 42 | 38, 41 | eqtri 2765 | . . . . . . 7
⊢ ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘3) = (𝑏‘𝑍) | 
| 43 | 28, 35, 42 | 3pm3.2i 1340 | . . . . . 6
⊢ (((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘1) = (𝑏‘𝑋) ∧ ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘2) = (𝑏‘𝑌) ∧ ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘3) = (𝑏‘𝑍)) | 
| 44 |  | fveq1 6905 | . . . . . . . 8
⊢ (𝑎 = (𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}) → (𝑎‘1) = ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘1)) | 
| 45 | 44 | eqeq1d 2739 | . . . . . . 7
⊢ (𝑎 = (𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}) → ((𝑎‘1) = (𝑏‘𝑋) ↔ ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘1) = (𝑏‘𝑋))) | 
| 46 |  | fveq1 6905 | . . . . . . . 8
⊢ (𝑎 = (𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}) → (𝑎‘2) = ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘2)) | 
| 47 | 46 | eqeq1d 2739 | . . . . . . 7
⊢ (𝑎 = (𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}) → ((𝑎‘2) = (𝑏‘𝑌) ↔ ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘2) = (𝑏‘𝑌))) | 
| 48 |  | fveq1 6905 | . . . . . . . 8
⊢ (𝑎 = (𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}) → (𝑎‘3) = ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘3)) | 
| 49 | 48 | eqeq1d 2739 | . . . . . . 7
⊢ (𝑎 = (𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}) → ((𝑎‘3) = (𝑏‘𝑍) ↔ ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘3) = (𝑏‘𝑍))) | 
| 50 | 45, 47, 49 | 3anbi123d 1438 | . . . . . 6
⊢ (𝑎 = (𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}) → (((𝑎‘1) = (𝑏‘𝑋) ∧ (𝑎‘2) = (𝑏‘𝑌) ∧ (𝑎‘3) = (𝑏‘𝑍)) ↔ (((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘1) = (𝑏‘𝑋) ∧ ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘2) = (𝑏‘𝑌) ∧ ((𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉})‘3) = (𝑏‘𝑍)))) | 
| 51 | 43, 50 | mpbiri 258 | . . . . 5
⊢ (𝑎 = (𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}) → ((𝑎‘1) = (𝑏‘𝑋) ∧ (𝑎‘2) = (𝑏‘𝑌) ∧ (𝑎‘3) = (𝑏‘𝑍))) | 
| 52 |  | rabren3dioph.a | . . . . 5
⊢ (((𝑎‘1) = (𝑏‘𝑋) ∧ (𝑎‘2) = (𝑏‘𝑌) ∧ (𝑎‘3) = (𝑏‘𝑍)) → (𝜑 ↔ 𝜓)) | 
| 53 | 51, 52 | syl 17 | . . . 4
⊢ (𝑎 = (𝑏 ∘ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}) → (𝜑 ↔ 𝜓)) | 
| 54 | 3, 53 | sbcie 3830 | . . 3
⊢
([(𝑏 ∘
{〈1, 𝑋〉, 〈2,
𝑌〉, 〈3, 𝑍〉}) / 𝑎]𝜑 ↔ 𝜓) | 
| 55 | 54 | rabbii 3442 | . 2
⊢ {𝑏 ∈ (ℕ0
↑m (1...𝑁))
∣ [(𝑏 ∘
{〈1, 𝑋〉, 〈2,
𝑌〉, 〈3, 𝑍〉}) / 𝑎]𝜑} = {𝑏 ∈ (ℕ0
↑m (1...𝑁))
∣ 𝜓} | 
| 56 | 11, 12, 13, 15, 17, 19, 4, 7, 10 | ftp 7177 | . . . . 5
⊢ {〈1,
𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}:{1, 2, 3}⟶{𝑋, 𝑌, 𝑍} | 
| 57 |  | 1z 12647 | . . . . . . . 8
⊢ 1 ∈
ℤ | 
| 58 |  | fztp 13620 | . . . . . . . 8
⊢ (1 ∈
ℤ → (1...(1 + 2)) = {1, (1 + 1), (1 + 2)}) | 
| 59 | 57, 58 | ax-mp 5 | . . . . . . 7
⊢ (1...(1 +
2)) = {1, (1 + 1), (1 + 2)} | 
| 60 |  | 1p2e3 12409 | . . . . . . . 8
⊢ (1 + 2) =
3 | 
| 61 | 60 | oveq2i 7442 | . . . . . . 7
⊢ (1...(1 +
2)) = (1...3) | 
| 62 |  | eqidd 2738 | . . . . . . . . 9
⊢ (1 ∈
ℤ → 1 = 1) | 
| 63 |  | 1p1e2 12391 | . . . . . . . . . 10
⊢ (1 + 1) =
2 | 
| 64 | 63 | a1i 11 | . . . . . . . . 9
⊢ (1 ∈
ℤ → (1 + 1) = 2) | 
| 65 | 60 | a1i 11 | . . . . . . . . 9
⊢ (1 ∈
ℤ → (1 + 2) = 3) | 
| 66 | 62, 64, 65 | tpeq123d 4748 | . . . . . . . 8
⊢ (1 ∈
ℤ → {1, (1 + 1), (1 + 2)} = {1, 2, 3}) | 
| 67 | 57, 66 | ax-mp 5 | . . . . . . 7
⊢ {1, (1 +
1), (1 + 2)} = {1, 2, 3} | 
| 68 | 59, 61, 67 | 3eqtr3i 2773 | . . . . . 6
⊢ (1...3) =
{1, 2, 3} | 
| 69 | 68 | feq2i 6728 | . . . . 5
⊢
({〈1, 𝑋〉,
〈2, 𝑌〉, 〈3,
𝑍〉}:(1...3)⟶{𝑋, 𝑌, 𝑍} ↔ {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}:{1, 2, 3}⟶{𝑋, 𝑌, 𝑍}) | 
| 70 | 56, 69 | mpbir 231 | . . . 4
⊢ {〈1,
𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}:(1...3)⟶{𝑋, 𝑌, 𝑍} | 
| 71 | 14, 16, 18 | 3pm3.2i 1340 | . . . . 5
⊢ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑍 ∈ (1...𝑁)) | 
| 72 | 15, 17, 19 | tpss 4837 | . . . . 5
⊢ ((𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑍 ∈ (1...𝑁)) ↔ {𝑋, 𝑌, 𝑍} ⊆ (1...𝑁)) | 
| 73 | 71, 72 | mpbi 230 | . . . 4
⊢ {𝑋, 𝑌, 𝑍} ⊆ (1...𝑁) | 
| 74 |  | fss 6752 | . . . 4
⊢
(({〈1, 𝑋〉,
〈2, 𝑌〉, 〈3,
𝑍〉}:(1...3)⟶{𝑋, 𝑌, 𝑍} ∧ {𝑋, 𝑌, 𝑍} ⊆ (1...𝑁)) → {〈1, 𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}:(1...3)⟶(1...𝑁)) | 
| 75 | 70, 73, 74 | mp2an 692 | . . 3
⊢ {〈1,
𝑋〉, 〈2, 𝑌〉, 〈3, 𝑍〉}:(1...3)⟶(1...𝑁) | 
| 76 |  | rabrenfdioph 42825 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ {〈1, 𝑋〉,
〈2, 𝑌〉, 〈3,
𝑍〉}:(1...3)⟶(1...𝑁) ∧ {𝑎 ∈ (ℕ0
↑m (1...3)) ∣ 𝜑} ∈ (Dioph‘3)) → {𝑏 ∈ (ℕ0
↑m (1...𝑁))
∣ [(𝑏 ∘
{〈1, 𝑋〉, 〈2,
𝑌〉, 〈3, 𝑍〉}) / 𝑎]𝜑} ∈ (Dioph‘𝑁)) | 
| 77 | 75, 76 | mp3an2 1451 | . 2
⊢ ((𝑁 ∈ ℕ0
∧ {𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ 𝜑} ∈ (Dioph‘3)) → {𝑏 ∈ (ℕ0
↑m (1...𝑁))
∣ [(𝑏 ∘
{〈1, 𝑋〉, 〈2,
𝑌〉, 〈3, 𝑍〉}) / 𝑎]𝜑} ∈ (Dioph‘𝑁)) | 
| 78 | 55, 77 | eqeltrrid 2846 | 1
⊢ ((𝑁 ∈ ℕ0
∧ {𝑎 ∈
(ℕ0 ↑m (1...3)) ∣ 𝜑} ∈ (Dioph‘3)) → {𝑏 ∈ (ℕ0
↑m (1...𝑁))
∣ 𝜓} ∈
(Dioph‘𝑁)) |