Step | Hyp | Ref
| Expression |
1 | | gexval.4 |
. 2
⊢ 𝐸 = (gEx‘𝐺) |
2 | | df-gex 18921 |
. . 3
⊢ gEx =
(𝑔 ∈ V ↦
⦋{𝑦 ∈
ℕ ∣ ∀𝑥
∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) |
3 | | nnex 11836 |
. . . . . 6
⊢ ℕ
∈ V |
4 | 3 | rabex 5225 |
. . . . 5
⊢ {𝑦 ∈ ℕ ∣
∀𝑥 ∈
(Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} ∈ V |
5 | 4 | a1i 11 |
. . . 4
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} ∈ V) |
6 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
7 | 6 | fveq2d 6721 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (Base‘𝑔) = (Base‘𝐺)) |
8 | | gexval.1 |
. . . . . . . . . . . 12
⊢ 𝑋 = (Base‘𝐺) |
9 | 7, 8 | eqtr4di 2796 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (Base‘𝑔) = 𝑋) |
10 | 6 | fveq2d 6721 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (.g‘𝑔) = (.g‘𝐺)) |
11 | | gexval.2 |
. . . . . . . . . . . . . 14
⊢ · =
(.g‘𝐺) |
12 | 10, 11 | eqtr4di 2796 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (.g‘𝑔) = · ) |
13 | 12 | oveqd 7230 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (𝑦(.g‘𝑔)𝑥) = (𝑦 · 𝑥)) |
14 | 6 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (0g‘𝑔) = (0g‘𝐺)) |
15 | | gexval.3 |
. . . . . . . . . . . . 13
⊢ 0 =
(0g‘𝐺) |
16 | 14, 15 | eqtr4di 2796 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (0g‘𝑔) = 0 ) |
17 | 13, 16 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → ((𝑦(.g‘𝑔)𝑥) = (0g‘𝑔) ↔ (𝑦 · 𝑥) = 0 )) |
18 | 9, 17 | raleqbidv 3313 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔) ↔ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 )) |
19 | 18 | rabbidv 3390 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 }) |
20 | | gexval.i |
. . . . . . . . 9
⊢ 𝐼 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } |
21 | 19, 20 | eqtr4di 2796 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} = 𝐼) |
22 | 21 | eqeq2d 2748 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → (𝑖 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} ↔ 𝑖 = 𝐼)) |
23 | 22 | biimpa 480 |
. . . . . 6
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) ∧ 𝑖 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)}) → 𝑖 = 𝐼) |
24 | 23 | eqeq1d 2739 |
. . . . 5
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) ∧ 𝑖 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)}) → (𝑖 = ∅ ↔ 𝐼 = ∅)) |
25 | 23 | infeq1d 9093 |
. . . . 5
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) ∧ 𝑖 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)}) → inf(𝑖, ℝ, < ) = inf(𝐼, ℝ, < )) |
26 | 24, 25 | ifbieq2d 4465 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) ∧ 𝑖 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)}) → if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )) = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < ))) |
27 | 5, 26 | csbied 3849 |
. . 3
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑔 = 𝐺) → ⦋{𝑦 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑦(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )) = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < ))) |
28 | | elex 3426 |
. . 3
⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V) |
29 | | c0ex 10827 |
. . . . 5
⊢ 0 ∈
V |
30 | | ltso 10913 |
. . . . . 6
⊢ < Or
ℝ |
31 | 30 | infex 9109 |
. . . . 5
⊢ inf(𝐼, ℝ, < ) ∈
V |
32 | 29, 31 | ifex 4489 |
. . . 4
⊢ if(𝐼 = ∅, 0, inf(𝐼, ℝ, < )) ∈
V |
33 | 32 | a1i 11 |
. . 3
⊢ (𝐺 ∈ 𝑉 → if(𝐼 = ∅, 0, inf(𝐼, ℝ, < )) ∈
V) |
34 | 2, 27, 28, 33 | fvmptd2 6826 |
. 2
⊢ (𝐺 ∈ 𝑉 → (gEx‘𝐺) = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < ))) |
35 | 1, 34 | syl5eq 2790 |
1
⊢ (𝐺 ∈ 𝑉 → 𝐸 = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < ))) |