Step | Hyp | Ref
| Expression |
1 | | gexval.4 |
. 2
⊢ 𝐸 = (gEx‘𝐺) |
2 | | df-gex 17949 |
. . . 4
⊢ gEx =
(𝑔 ∈ V ↦
⦋{𝑦 ∈
ℕ ∣ ∀𝑥
∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝐺 ∈ 𝑉 → gEx = (𝑔 ∈ V ↦ ⦋{𝑦 ∈ ℕ ∣
∀𝑥 ∈
(Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))) |
4 | | nnex 11026 |
. . . . . 6
⊢ ℕ
∈ V |
5 | 4 | rabex 4813 |
. . . . 5
⊢ {𝑦 ∈ ℕ ∣
∀𝑥 ∈
(Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} ∈ V |
6 | 5 | a1i 11 |
. . . 4
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} ∈ V) |
7 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
8 | 7 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (Base‘𝑔) = (Base‘𝐺)) |
9 | | gexval.1 |
. . . . . . . . . . . 12
⊢ 𝑋 = (Base‘𝐺) |
10 | 8, 9 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (Base‘𝑔) = 𝑋) |
11 | 7 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (.g‘𝑔) = (.g‘𝐺)) |
12 | | gexval.2 |
. . . . . . . . . . . . . 14
⊢ · =
(.g‘𝐺) |
13 | 11, 12 | syl6eqr 2674 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (.g‘𝑔) = · ) |
14 | 13 | oveqd 6667 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (𝑦(.g‘𝑔)𝑥) = (𝑦 · 𝑥)) |
15 | 7 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (0g‘𝑔) = (0g‘𝐺)) |
16 | | gexval.3 |
. . . . . . . . . . . . 13
⊢ 0 =
(0g‘𝐺) |
17 | 15, 16 | syl6eqr 2674 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (0g‘𝑔) = 0 ) |
18 | 14, 17 | eqeq12d 2637 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → ((𝑦(.g‘𝑔)𝑥) = (0g‘𝑔) ↔ (𝑦 · 𝑥) = 0 )) |
19 | 10, 18 | raleqbidv 3152 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔) ↔ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 )) |
20 | 19 | rabbidv 3189 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 }) |
21 | | gexval.i |
. . . . . . . . 9
⊢ 𝐼 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } |
22 | 20, 21 | syl6eqr 2674 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} = 𝐼) |
23 | 22 | eqeq2d 2632 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (𝑖 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} ↔ 𝑖 = 𝐼)) |
24 | 23 | biimpa 501 |
. . . . . 6
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) ∧ 𝑖 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)}) → 𝑖 = 𝐼) |
25 | 24 | eqeq1d 2624 |
. . . . 5
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) ∧ 𝑖 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)}) → (𝑖 = ∅ ↔ 𝐼 = ∅)) |
26 | 24 | infeq1d 8383 |
. . . . 5
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) ∧ 𝑖 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)}) → inf(𝑖, ℝ, < ) = inf(𝐼, ℝ, < )) |
27 | 25, 26 | ifbieq2d 4111 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) ∧ 𝑖 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)}) → if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )) = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < ))) |
28 | 6, 27 | csbied 3560 |
. . 3
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → ⦋{𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )) = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < ))) |
29 | | elex 3212 |
. . 3
⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V) |
30 | | c0ex 10034 |
. . . . 5
⊢ 0 ∈
V |
31 | | ltso 10118 |
. . . . . 6
⊢ < Or
ℝ |
32 | 31 | infex 8399 |
. . . . 5
⊢ inf(𝐼, ℝ, < ) ∈
V |
33 | 30, 32 | ifex 4156 |
. . . 4
⊢ if(𝐼 = ∅, 0, inf(𝐼, ℝ, < )) ∈
V |
34 | 33 | a1i 11 |
. . 3
⊢ (𝐺 ∈ 𝑉 → if(𝐼 = ∅, 0, inf(𝐼, ℝ, < )) ∈
V) |
35 | 3, 28, 29, 34 | fvmptd 6288 |
. 2
⊢ (𝐺 ∈ 𝑉 → (gEx‘𝐺) = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < ))) |
36 | 1, 35 | syl5eq 2668 |
1
⊢ (𝐺 ∈ 𝑉 → 𝐸 = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < ))) |