Step |
Hyp |
Ref |
Expression |
0 |
|
cidl |
⊢ Idl |
1 |
|
vr |
⊢ 𝑟 |
2 |
|
crngo |
⊢ RingOps |
3 |
|
vi |
⊢ 𝑖 |
4 |
|
c1st |
⊢ 1st |
5 |
1
|
cv |
⊢ 𝑟 |
6 |
5 4
|
cfv |
⊢ ( 1st ‘ 𝑟 ) |
7 |
6
|
crn |
⊢ ran ( 1st ‘ 𝑟 ) |
8 |
7
|
cpw |
⊢ 𝒫 ran ( 1st ‘ 𝑟 ) |
9 |
|
cgi |
⊢ GId |
10 |
6 9
|
cfv |
⊢ ( GId ‘ ( 1st ‘ 𝑟 ) ) |
11 |
3
|
cv |
⊢ 𝑖 |
12 |
10 11
|
wcel |
⊢ ( GId ‘ ( 1st ‘ 𝑟 ) ) ∈ 𝑖 |
13 |
|
vx |
⊢ 𝑥 |
14 |
|
vy |
⊢ 𝑦 |
15 |
13
|
cv |
⊢ 𝑥 |
16 |
14
|
cv |
⊢ 𝑦 |
17 |
15 16 6
|
co |
⊢ ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) |
18 |
17 11
|
wcel |
⊢ ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 |
19 |
18 14 11
|
wral |
⊢ ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 |
20 |
|
vz |
⊢ 𝑧 |
21 |
20
|
cv |
⊢ 𝑧 |
22 |
|
c2nd |
⊢ 2nd |
23 |
5 22
|
cfv |
⊢ ( 2nd ‘ 𝑟 ) |
24 |
21 15 23
|
co |
⊢ ( 𝑧 ( 2nd ‘ 𝑟 ) 𝑥 ) |
25 |
24 11
|
wcel |
⊢ ( 𝑧 ( 2nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 |
26 |
15 21 23
|
co |
⊢ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑧 ) |
27 |
26 11
|
wcel |
⊢ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 |
28 |
25 27
|
wa |
⊢ ( ( 𝑧 ( 2nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) |
29 |
28 20 7
|
wral |
⊢ ∀ 𝑧 ∈ ran ( 1st ‘ 𝑟 ) ( ( 𝑧 ( 2nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) |
30 |
19 29
|
wa |
⊢ ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1st ‘ 𝑟 ) ( ( 𝑧 ( 2nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) |
31 |
30 13 11
|
wral |
⊢ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1st ‘ 𝑟 ) ( ( 𝑧 ( 2nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) |
32 |
12 31
|
wa |
⊢ ( ( GId ‘ ( 1st ‘ 𝑟 ) ) ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1st ‘ 𝑟 ) ( ( 𝑧 ( 2nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) ) |
33 |
32 3 8
|
crab |
⊢ { 𝑖 ∈ 𝒫 ran ( 1st ‘ 𝑟 ) ∣ ( ( GId ‘ ( 1st ‘ 𝑟 ) ) ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1st ‘ 𝑟 ) ( ( 𝑧 ( 2nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) ) } |
34 |
1 2 33
|
cmpt |
⊢ ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ 𝒫 ran ( 1st ‘ 𝑟 ) ∣ ( ( GId ‘ ( 1st ‘ 𝑟 ) ) ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1st ‘ 𝑟 ) ( ( 𝑧 ( 2nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) ) } ) |
35 |
0 34
|
wceq |
⊢ Idl = ( 𝑟 ∈ RingOps ↦ { 𝑖 ∈ 𝒫 ran ( 1st ‘ 𝑟 ) ∣ ( ( GId ‘ ( 1st ‘ 𝑟 ) ) ∈ 𝑖 ∧ ∀ 𝑥 ∈ 𝑖 ( ∀ 𝑦 ∈ 𝑖 ( 𝑥 ( 1st ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ∧ ∀ 𝑧 ∈ ran ( 1st ‘ 𝑟 ) ( ( 𝑧 ( 2nd ‘ 𝑟 ) 𝑥 ) ∈ 𝑖 ∧ ( 𝑥 ( 2nd ‘ 𝑟 ) 𝑧 ) ∈ 𝑖 ) ) ) } ) |