Step |
Hyp |
Ref |
Expression |
0 |
|
cmaxidl |
⊢ MaxIdl |
1 |
|
vr |
⊢ 𝑟 |
2 |
|
crngo |
⊢ RingOps |
3 |
|
vi |
⊢ 𝑖 |
4 |
|
cidl |
⊢ Idl |
5 |
1
|
cv |
⊢ 𝑟 |
6 |
5 4
|
cfv |
⊢ ( Idl ‘ 𝑟 ) |
7 |
3
|
cv |
⊢ 𝑖 |
8 |
|
c1st |
⊢ 1st |
9 |
5 8
|
cfv |
⊢ ( 1st ‘ 𝑟 ) |
10 |
9
|
crn |
⊢ ran ( 1st ‘ 𝑟 ) |
11 |
7 10
|
wne |
⊢ 𝑖 ≠ ran ( 1st ‘ 𝑟 ) |
12 |
|
vj |
⊢ 𝑗 |
13 |
12
|
cv |
⊢ 𝑗 |
14 |
7 13
|
wss |
⊢ 𝑖 ⊆ 𝑗 |
15 |
13 7
|
wceq |
⊢ 𝑗 = 𝑖 |
16 |
13 10
|
wceq |
⊢ 𝑗 = ran ( 1st ‘ 𝑟 ) |
17 |
15 16
|
wo |
⊢ ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1st ‘ 𝑟 ) ) |
18 |
14 17
|
wi |
⊢ ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1st ‘ 𝑟 ) ) ) |
19 |
18 12 6
|
wral |
⊢ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1st ‘ 𝑟 ) ) ) |
20 |
11 19
|
wa |
⊢ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1st ‘ 𝑟 ) ) ) ) |
21 |
20 3 6
|
crab |
⊢ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1st ‘ 𝑟 ) ) ) ) } |
22 |
1 2 21
|
cmpt |
⊢ ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1st ‘ 𝑟 ) ) ) ) } ) |
23 |
0 22
|
wceq |
⊢ MaxIdl = ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ ( Idl ‘ 𝑟 ) ∣ ( 𝑖 ≠ ran ( 1st ‘ 𝑟 ) ∧ ∀ 𝑗 ∈ ( Idl ‘ 𝑟 ) ( 𝑖 ⊆ 𝑗 → ( 𝑗 = 𝑖 ∨ 𝑗 = ran ( 1st ‘ 𝑟 ) ) ) ) } ) |