| Step | Hyp | Ref
| Expression |
| 1 | | gexval.4 |
. 2
⊢ 𝐸 = (gEx‘𝐺) |
| 2 | | df-gex 19547 |
. . 3
⊢ gEx =
(𝑔 ∈ V ↦
⦋{𝑦 ∈
ℕ ∣ ∀𝑥
∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) |
| 3 | | nnex 12272 |
. . . . . 6
⊢ ℕ
∈ V |
| 4 | 3 | rabex 5339 |
. . . . 5
⊢ {𝑦 ∈ ℕ ∣
∀𝑥 ∈
(Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} ∈ V |
| 5 | 4 | a1i 11 |
. . . 4
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} ∈ V) |
| 6 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
| 7 | 6 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (Base‘𝑔) = (Base‘𝐺)) |
| 8 | | gexval.1 |
. . . . . . . . . . . 12
⊢ 𝑋 = (Base‘𝐺) |
| 9 | 7, 8 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (Base‘𝑔) = 𝑋) |
| 10 | 6 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (.g‘𝑔) = (.g‘𝐺)) |
| 11 | | gexval.2 |
. . . . . . . . . . . . . 14
⊢ · =
(.g‘𝐺) |
| 12 | 10, 11 | eqtr4di 2795 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (.g‘𝑔) = · ) |
| 13 | 12 | oveqd 7448 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (𝑦(.g‘𝑔)𝑥) = (𝑦 · 𝑥)) |
| 14 | 6 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (0g‘𝑔) = (0g‘𝐺)) |
| 15 | | gexval.3 |
. . . . . . . . . . . . 13
⊢ 0 =
(0g‘𝐺) |
| 16 | 14, 15 | eqtr4di 2795 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (0g‘𝑔) = 0 ) |
| 17 | 13, 16 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → ((𝑦(.g‘𝑔)𝑥) = (0g‘𝑔) ↔ (𝑦 · 𝑥) = 0 )) |
| 18 | 9, 17 | raleqbidv 3346 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔) ↔ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 )) |
| 19 | 18 | rabbidv 3444 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 }) |
| 20 | | gexval.i |
. . . . . . . . 9
⊢ 𝐼 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } |
| 21 | 19, 20 | eqtr4di 2795 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} = 𝐼) |
| 22 | 21 | eqeq2d 2748 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (𝑖 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} ↔ 𝑖 = 𝐼)) |
| 23 | 22 | biimpa 476 |
. . . . . 6
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) ∧ 𝑖 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)}) → 𝑖 = 𝐼) |
| 24 | 23 | eqeq1d 2739 |
. . . . 5
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) ∧ 𝑖 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)}) → (𝑖 = ∅ ↔ 𝐼 = ∅)) |
| 25 | 23 | infeq1d 9517 |
. . . . 5
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) ∧ 𝑖 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)}) → inf(𝑖, ℝ, < ) = inf(𝐼, ℝ, < )) |
| 26 | 24, 25 | ifbieq2d 4552 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) ∧ 𝑖 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)}) → if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )) = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < ))) |
| 27 | 5, 26 | csbied 3935 |
. . 3
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → ⦋{𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )) = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < ))) |
| 28 | | elex 3501 |
. . 3
⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V) |
| 29 | | c0ex 11255 |
. . . . 5
⊢ 0 ∈
V |
| 30 | | ltso 11341 |
. . . . . 6
⊢ < Or
ℝ |
| 31 | 30 | infex 9533 |
. . . . 5
⊢ inf(𝐼, ℝ, < ) ∈
V |
| 32 | 29, 31 | ifex 4576 |
. . . 4
⊢ if(𝐼 = ∅, 0, inf(𝐼, ℝ, < )) ∈
V |
| 33 | 32 | a1i 11 |
. . 3
⊢ (𝐺 ∈ 𝑉 → if(𝐼 = ∅, 0, inf(𝐼, ℝ, < )) ∈
V) |
| 34 | 2, 27, 28, 33 | fvmptd2 7024 |
. 2
⊢ (𝐺 ∈ 𝑉 → (gEx‘𝐺) = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < ))) |
| 35 | 1, 34 | eqtrid 2789 |
1
⊢ (𝐺 ∈ 𝑉 → 𝐸 = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < ))) |