Step |
Hyp |
Ref |
Expression |
0 |
|
cgex |
⊢ gEx |
1 |
|
vg |
⊢ 𝑔 |
2 |
|
cvv |
⊢ V |
3 |
|
vn |
⊢ 𝑛 |
4 |
|
cn |
⊢ ℕ |
5 |
|
vx |
⊢ 𝑥 |
6 |
|
cbs |
⊢ Base |
7 |
1
|
cv |
⊢ 𝑔 |
8 |
7 6
|
cfv |
⊢ ( Base ‘ 𝑔 ) |
9 |
3
|
cv |
⊢ 𝑛 |
10 |
|
cmg |
⊢ .g |
11 |
7 10
|
cfv |
⊢ ( .g ‘ 𝑔 ) |
12 |
5
|
cv |
⊢ 𝑥 |
13 |
9 12 11
|
co |
⊢ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) |
14 |
|
c0g |
⊢ 0g |
15 |
7 14
|
cfv |
⊢ ( 0g ‘ 𝑔 ) |
16 |
13 15
|
wceq |
⊢ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) |
17 |
16 5 8
|
wral |
⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) |
18 |
17 3 4
|
crab |
⊢ { 𝑛 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } |
19 |
|
vi |
⊢ 𝑖 |
20 |
19
|
cv |
⊢ 𝑖 |
21 |
|
c0 |
⊢ ∅ |
22 |
20 21
|
wceq |
⊢ 𝑖 = ∅ |
23 |
|
cc0 |
⊢ 0 |
24 |
|
cr |
⊢ ℝ |
25 |
|
clt |
⊢ < |
26 |
20 24 25
|
cinf |
⊢ inf ( 𝑖 , ℝ , < ) |
27 |
22 23 26
|
cif |
⊢ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) |
28 |
19 18 27
|
csb |
⊢ ⦋ { 𝑛 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) |
29 |
1 2 28
|
cmpt |
⊢ ( 𝑔 ∈ V ↦ ⦋ { 𝑛 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) |
30 |
0 29
|
wceq |
⊢ gEx = ( 𝑔 ∈ V ↦ ⦋ { 𝑛 ∈ ℕ ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) = ( 0g ‘ 𝑔 ) } / 𝑖 ⦌ if ( 𝑖 = ∅ , 0 , inf ( 𝑖 , ℝ , < ) ) ) |