Step | Hyp | Ref
| Expression |

1 | | cmaxidl 35405 |
. 2
class
MaxIdl |

2 | | vr |
. . 3
setvar 𝑟 |

3 | | crngo 35290 |
. . 3
class
RingOps |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

18 | | cidl 35403 |
. . . . . . 7
class
Idl |

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

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

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

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

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

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