Step | Hyp | Ref
| Expression |

1 | | cmaxidl 34437 |
. 2
class
MaxIdl |

2 | | vr |
. . 3
setvar 𝑟 |

3 | | crngo 34322 |
. . 3
class
RingOps |

4 | | vi |
. . . . . . 7
setvar 𝑖 |

5 | 4 | cv 1600 |
. . . . . 6
class 𝑖 |

6 | 2 | cv 1600 |
. . . . . . . 8
class 𝑟 |

7 | | c1st 7445 |
. . . . . . . 8
class
1^{st} |

8 | 6, 7 | cfv 6137 |
. . . . . . 7
class
(1^{st} ‘𝑟) |

9 | 8 | crn 5358 |
. . . . . 6
class ran
(1^{st} ‘𝑟) |

10 | 5, 9 | wne 2969 |
. . . . 5
wff 𝑖 ≠ ran (1^{st}
‘𝑟) |

11 | | vj |
. . . . . . . . 9
setvar 𝑗 |

12 | 11 | cv 1600 |
. . . . . . . 8
class 𝑗 |

13 | 5, 12 | wss 3792 |
. . . . . . 7
wff 𝑖 ⊆ 𝑗 |

14 | 11, 4 | weq 2005 |
. . . . . . . 8
wff 𝑗 = 𝑖 |

15 | 12, 9 | wceq 1601 |
. . . . . . . 8
wff 𝑗 = ran (1^{st}
‘𝑟) |

16 | 14, 15 | wo 836 |
. . . . . . 7
wff (𝑗 = 𝑖 ∨ 𝑗 = ran (1^{st} ‘𝑟)) |

17 | 13, 16 | wi 4 |
. . . . . 6
wff (𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1^{st} ‘𝑟))) |

18 | | cidl 34435 |
. . . . . . 7
class
Idl |

19 | 6, 18 | cfv 6137 |
. . . . . 6
class
(Idl‘𝑟) |

20 | 17, 11, 19 | wral 3090 |
. . . . 5
wff
∀𝑗 ∈
(Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1^{st} ‘𝑟))) |

21 | 10, 20 | wa 386 |
. . . 4
wff (𝑖 ≠ ran (1^{st}
‘𝑟) ∧
∀𝑗 ∈
(Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1^{st} ‘𝑟)))) |

22 | 21, 4, 19 | crab 3094 |
. . 3
class {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1^{st} ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1^{st} ‘𝑟))))} |

23 | 2, 3, 22 | cmpt 4967 |
. 2
class (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1^{st} ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1^{st} ‘𝑟))))}) |

24 | 1, 23 | wceq 1601 |
1
wff MaxIdl =
(𝑟 ∈ RingOps ↦
{𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1^{st} ‘𝑟) ∧ ∀𝑗 ∈ (Idl‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = ran (1^{st} ‘𝑟))))}) |