Proof of Theorem noinfdm
| Step | Hyp | Ref
| Expression |
| 1 | | noinfdm.1 |
. . . 4
⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
| 2 | | iffalse 4534 |
. . . 4
⊢ (¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
| 3 | 1, 2 | eqtrid 2789 |
. . 3
⊢ (¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → 𝑇 = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
| 4 | 3 | dmeqd 5916 |
. 2
⊢ (¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
| 5 | | iotaex 6534 |
. . . 4
⊢
(℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) ∈ V |
| 6 | | eqid 2737 |
. . . 4
⊢ (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) |
| 7 | 5, 6 | dmmpti 6712 |
. . 3
⊢ dom
(𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} |
| 8 | | eleq1w 2824 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (𝑦 ∈ dom 𝑢 ↔ 𝑧 ∈ dom 𝑢)) |
| 9 | | suceq 6450 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧) |
| 10 | 9 | reseq2d 5997 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑧)) |
| 11 | 9 | reseq2d 5997 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑧)) |
| 12 | 10, 11 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧))) |
| 13 | 12 | imbi2d 340 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧)))) |
| 14 | 13 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧)))) |
| 15 | 8, 14 | anbi12d 632 |
. . . . . 6
⊢ (𝑦 = 𝑧 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑧 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧))))) |
| 16 | 15 | rexbidv 3179 |
. . . . 5
⊢ (𝑦 = 𝑧 → (∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢 ∈ 𝐵 (𝑧 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧))))) |
| 17 | | dmeq 5914 |
. . . . . . . 8
⊢ (𝑢 = 𝑝 → dom 𝑢 = dom 𝑝) |
| 18 | 17 | eleq2d 2827 |
. . . . . . 7
⊢ (𝑢 = 𝑝 → (𝑧 ∈ dom 𝑢 ↔ 𝑧 ∈ dom 𝑝)) |
| 19 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑝 → (𝑢 <s 𝑣 ↔ 𝑝 <s 𝑣)) |
| 20 | 19 | notbid 318 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑝 → (¬ 𝑢 <s 𝑣 ↔ ¬ 𝑝 <s 𝑣)) |
| 21 | | reseq1 5991 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑝 → (𝑢 ↾ suc 𝑧) = (𝑝 ↾ suc 𝑧)) |
| 22 | 21 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑝 → ((𝑢 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧) ↔ (𝑝 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧))) |
| 23 | 20, 22 | imbi12d 344 |
. . . . . . . . 9
⊢ (𝑢 = 𝑝 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧)) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧)))) |
| 24 | 23 | ralbidv 3178 |
. . . . . . . 8
⊢ (𝑢 = 𝑝 → (∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧)))) |
| 25 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑞 → (𝑝 <s 𝑣 ↔ 𝑝 <s 𝑞)) |
| 26 | 25 | notbid 318 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑞 → (¬ 𝑝 <s 𝑣 ↔ ¬ 𝑝 <s 𝑞)) |
| 27 | | reseq1 5991 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑞 → (𝑣 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)) |
| 28 | 27 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑞 → ((𝑝 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧) ↔ (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))) |
| 29 | 26, 28 | imbi12d 344 |
. . . . . . . . 9
⊢ (𝑣 = 𝑞 → ((¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧)) ↔ (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))) |
| 30 | 29 | cbvralvw 3237 |
. . . . . . . 8
⊢
(∀𝑣 ∈
𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧)) ↔ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))) |
| 31 | 24, 30 | bitrdi 287 |
. . . . . . 7
⊢ (𝑢 = 𝑝 → (∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧)) ↔ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))) |
| 32 | 18, 31 | anbi12d 632 |
. . . . . 6
⊢ (𝑢 = 𝑝 → ((𝑧 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧))) ↔ (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))))) |
| 33 | 32 | cbvrexvw 3238 |
. . . . 5
⊢
(∃𝑢 ∈
𝐵 (𝑧 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑧) = (𝑣 ↾ suc 𝑧))) ↔ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))) |
| 34 | 16, 33 | bitrdi 287 |
. . . 4
⊢ (𝑦 = 𝑧 → (∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))))) |
| 35 | 34 | cbvabv 2812 |
. . 3
⊢ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} = {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))} |
| 36 | 7, 35 | eqtri 2765 |
. 2
⊢ dom
(𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))} |
| 37 | 4, 36 | eqtrdi 2793 |
1
⊢ (¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))}) |