Step | Hyp | Ref
| Expression |
1 | | odval.4 |
. 2
⊢ 𝑂 = (od‘𝐺) |
2 | | fveq2 6717 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
3 | | odval.1 |
. . . . . 6
⊢ 𝑋 = (Base‘𝐺) |
4 | 2, 3 | eqtr4di 2796 |
. . . . 5
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑋) |
5 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (.g‘𝑔) = (.g‘𝐺)) |
6 | | odval.2 |
. . . . . . . . . 10
⊢ · =
(.g‘𝐺) |
7 | 5, 6 | eqtr4di 2796 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (.g‘𝑔) = · ) |
8 | 7 | oveqd 7230 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (𝑦(.g‘𝑔)𝑥) = (𝑦 · 𝑥)) |
9 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (0g‘𝑔) = (0g‘𝐺)) |
10 | | odval.3 |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐺) |
11 | 9, 10 | eqtr4di 2796 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (0g‘𝑔) = 0 ) |
12 | 8, 11 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → ((𝑦(.g‘𝑔)𝑥) = (0g‘𝑔) ↔ (𝑦 · 𝑥) = 0 )) |
13 | 12 | rabbidv 3390 |
. . . . . 6
⊢ (𝑔 = 𝐺 → {𝑦 ∈ ℕ ∣ (𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} = {𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 }) |
14 | 13 | csbeq1d 3815 |
. . . . 5
⊢ (𝑔 = 𝐺 → ⦋{𝑦 ∈ ℕ ∣ (𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )) = ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) |
15 | 4, 14 | mpteq12dv 5140 |
. . . 4
⊢ (𝑔 = 𝐺 → (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) = (𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))) |
16 | | df-od 18920 |
. . . 4
⊢ od =
(𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))) |
17 | 3 | fvexi 6731 |
. . . . 5
⊢ 𝑋 ∈ V |
18 | | nn0ex 12096 |
. . . . 5
⊢
ℕ0 ∈ V |
19 | | nnex 11836 |
. . . . . . . . 9
⊢ ℕ
∈ V |
20 | 19 | rabex 5225 |
. . . . . . . 8
⊢ {𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } ∈
V |
21 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑖 = {𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } → (𝑖 = ∅ ↔ {𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } =
∅)) |
22 | | infeq1 9092 |
. . . . . . . . 9
⊢ (𝑖 = {𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } → inf(𝑖, ℝ, < ) = inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 }, ℝ, <
)) |
23 | 21, 22 | ifbieq2d 4465 |
. . . . . . . 8
⊢ (𝑖 = {𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } → if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )) = if({𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } = ∅, 0, inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 }, ℝ, <
))) |
24 | 20, 23 | csbie 3847 |
. . . . . . 7
⊢
⦋{𝑦
∈ ℕ ∣ (𝑦
·
𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )) = if({𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } = ∅, 0, inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 }, ℝ, <
)) |
25 | | 0nn0 12105 |
. . . . . . . . . 10
⊢ 0 ∈
ℕ0 |
26 | 25 | a1i 11 |
. . . . . . . . 9
⊢
((⊤ ∧ {𝑦
∈ ℕ ∣ (𝑦
·
𝑥) = 0 } = ∅) → 0
∈ ℕ0) |
27 | | df-ne 2941 |
. . . . . . . . . . . 12
⊢ ({𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } ≠ ∅ ↔
¬ {𝑦 ∈ ℕ
∣ (𝑦 · 𝑥) = 0 } =
∅) |
28 | | ssrab2 3993 |
. . . . . . . . . . . . 13
⊢ {𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } ⊆
ℕ |
29 | | nnuz 12477 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘1) |
30 | 28, 29 | sseqtri 3937 |
. . . . . . . . . . . . . 14
⊢ {𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } ⊆
(ℤ≥‘1) |
31 | | infssuzcl 12528 |
. . . . . . . . . . . . . 14
⊢ (({𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } ⊆
(ℤ≥‘1) ∧ {𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } ≠ ∅) →
inf({𝑦 ∈ ℕ
∣ (𝑦 · 𝑥) = 0 }, ℝ, < ) ∈
{𝑦 ∈ ℕ ∣
(𝑦 · 𝑥) = 0 }) |
32 | 30, 31 | mpan 690 |
. . . . . . . . . . . . 13
⊢ ({𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } ≠ ∅ →
inf({𝑦 ∈ ℕ
∣ (𝑦 · 𝑥) = 0 }, ℝ, < ) ∈
{𝑦 ∈ ℕ ∣
(𝑦 · 𝑥) = 0 }) |
33 | 28, 32 | sseldi 3899 |
. . . . . . . . . . . 12
⊢ ({𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } ≠ ∅ →
inf({𝑦 ∈ ℕ
∣ (𝑦 · 𝑥) = 0 }, ℝ, < ) ∈
ℕ) |
34 | 27, 33 | sylbir 238 |
. . . . . . . . . . 11
⊢ (¬
{𝑦 ∈ ℕ ∣
(𝑦 · 𝑥) = 0 } = ∅ →
inf({𝑦 ∈ ℕ
∣ (𝑦 · 𝑥) = 0 }, ℝ, < ) ∈
ℕ) |
35 | 34 | nnnn0d 12150 |
. . . . . . . . . 10
⊢ (¬
{𝑦 ∈ ℕ ∣
(𝑦 · 𝑥) = 0 } = ∅ →
inf({𝑦 ∈ ℕ
∣ (𝑦 · 𝑥) = 0 }, ℝ, < ) ∈
ℕ0) |
36 | 35 | adantl 485 |
. . . . . . . . 9
⊢
((⊤ ∧ ¬ {𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } = ∅) →
inf({𝑦 ∈ ℕ
∣ (𝑦 · 𝑥) = 0 }, ℝ, < ) ∈
ℕ0) |
37 | 26, 36 | ifclda 4474 |
. . . . . . . 8
⊢ (⊤
→ if({𝑦 ∈ ℕ
∣ (𝑦 · 𝑥) = 0 } = ∅, 0, inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 }, ℝ, < )) ∈
ℕ0) |
38 | 37 | mptru 1550 |
. . . . . . 7
⊢ if({𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } = ∅, 0, inf({𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 }, ℝ, < )) ∈
ℕ0 |
39 | 24, 38 | eqeltri 2834 |
. . . . . 6
⊢
⦋{𝑦
∈ ℕ ∣ (𝑦
·
𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )) ∈
ℕ0 |
40 | 39 | rgenw 3073 |
. . . . 5
⊢
∀𝑥 ∈
𝑋 ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )) ∈
ℕ0 |
41 | 17, 18, 40 | mptexw 7726 |
. . . 4
⊢ (𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) ∈ V |
42 | 15, 16, 41 | fvmpt 6818 |
. . 3
⊢ (𝐺 ∈ V → (od‘𝐺) = (𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))) |
43 | | fvprc 6709 |
. . . 4
⊢ (¬
𝐺 ∈ V →
(od‘𝐺) =
∅) |
44 | | fvprc 6709 |
. . . . . . 7
⊢ (¬
𝐺 ∈ V →
(Base‘𝐺) =
∅) |
45 | 3, 44 | syl5eq 2790 |
. . . . . 6
⊢ (¬
𝐺 ∈ V → 𝑋 = ∅) |
46 | 45 | mpteq1d 5144 |
. . . . 5
⊢ (¬
𝐺 ∈ V → (𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) = (𝑥 ∈ ∅ ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))) |
47 | | mpt0 6520 |
. . . . 5
⊢ (𝑥 ∈ ∅ ↦
⦋{𝑦 ∈
ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) =
∅ |
48 | 46, 47 | eqtrdi 2794 |
. . . 4
⊢ (¬
𝐺 ∈ V → (𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) =
∅) |
49 | 43, 48 | eqtr4d 2780 |
. . 3
⊢ (¬
𝐺 ∈ V →
(od‘𝐺) = (𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))) |
50 | 42, 49 | pm2.61i 185 |
. 2
⊢
(od‘𝐺) =
(𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) |
51 | 1, 50 | eqtri 2765 |
1
⊢ 𝑂 = (𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) |