Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aomclem8 Structured version   Visualization version   GIF version
Theorem aomclem8 41788
Description: Lemma for dfac11 41789. Perform variable substitutions. This is the most we can say without invoking regularity. (Contributed by Stefan O'Rear, 20-Jan-2015.)
Hypotheses
Ref Expression
aomclem8.a (πœ‘ β†’ 𝐴 ∈ On)
aomclem8.y (πœ‘ β†’ βˆ€π‘Ž ∈ 𝒫 (𝑅1β€˜π΄)(π‘Ž β‰  βˆ… β†’ (π‘¦β€˜π‘Ž) ∈ ((𝒫 π‘Ž ∩ Fin) βˆ– {βˆ…})))
Assertion
Ref Expression
aomclem8 (πœ‘ β†’ βˆƒπ‘ 𝑏 We (𝑅1β€˜π΄))
Distinct variable groups:   πœ‘,𝑏   𝐴,π‘Ž,𝑏   𝑦,π‘Ž,𝑏
Allowed substitution hints:   πœ‘(𝑦,π‘Ž)   𝐴(𝑦)
Proof of Theorem aomclem8
Dummy variables 𝑐 𝑑 𝑒 𝑓 𝑔 β„Ž 𝑖 𝑗 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elequ2 2121 . . . . . . 7 (β„Ž = 𝑏 β†’ (𝑖 ∈ β„Ž ↔ 𝑖 ∈ 𝑏))
2 elequ2 2121 . . . . . . . 8 (𝑔 = 𝑐 β†’ (𝑖 ∈ 𝑔 ↔ 𝑖 ∈ 𝑐))
32notbid 317 . . . . . . 7 (𝑔 = 𝑐 β†’ (Β¬ 𝑖 ∈ 𝑔 ↔ Β¬ 𝑖 ∈ 𝑐))
41, 3bi2anan9r 638 . . . . . 6 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ ((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ↔ (𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐)))
5 elequ2 2121 . . . . . . . . 9 (𝑔 = 𝑐 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ 𝑐))
6 elequ2 2121 . . . . . . . . 9 (β„Ž = 𝑏 β†’ (𝑗 ∈ β„Ž ↔ 𝑗 ∈ 𝑏))
75, 6bi2bian9 639 . . . . . . . 8 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ ((𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž) ↔ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)))
87imbi2d 340 . . . . . . 7 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ ((𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)) ↔ (𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))))
98ralbidv 3177 . . . . . 6 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)) ↔ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))))
104, 9anbi12d 631 . . . . 5 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))) ↔ ((𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)))))
1110rexbidv 3178 . . . 4 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))) ↔ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)))))
12 elequ1 2113 . . . . . . 7 (𝑖 = 𝑑 β†’ (𝑖 ∈ 𝑏 ↔ 𝑑 ∈ 𝑏))
13 elequ1 2113 . . . . . . . 8 (𝑖 = 𝑑 β†’ (𝑖 ∈ 𝑐 ↔ 𝑑 ∈ 𝑐))
1413notbid 317 . . . . . . 7 (𝑖 = 𝑑 β†’ (Β¬ 𝑖 ∈ 𝑐 ↔ Β¬ 𝑑 ∈ 𝑐))
1512, 14anbi12d 631 . . . . . 6 (𝑖 = 𝑑 β†’ ((𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐) ↔ (𝑑 ∈ 𝑏 ∧ Β¬ 𝑑 ∈ 𝑐)))
16 breq2 5151 . . . . . . . . 9 (𝑖 = 𝑑 β†’ (𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 ↔ 𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑))
1716imbi1d 341 . . . . . . . 8 (𝑖 = 𝑑 β†’ ((𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)) ↔ (𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))))
1817ralbidv 3177 . . . . . . 7 (𝑖 = 𝑑 β†’ (βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)) ↔ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))))
19 breq1 5150 . . . . . . . . 9 (𝑗 = 𝑓 β†’ (𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑 ↔ 𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑))
20 elequ1 2113 . . . . . . . . . 10 (𝑗 = 𝑓 β†’ (𝑗 ∈ 𝑐 ↔ 𝑓 ∈ 𝑐))
21 elequ1 2113 . . . . . . . . . 10 (𝑗 = 𝑓 β†’ (𝑗 ∈ 𝑏 ↔ 𝑓 ∈ 𝑏))
2220, 21bibi12d 345 . . . . . . . . 9 (𝑗 = 𝑓 β†’ ((𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏) ↔ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏)))
2319, 22imbi12d 344 . . . . . . . 8 (𝑗 = 𝑓 β†’ ((𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)) ↔ (𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏))))
2423cbvralvw 3234 . . . . . . 7 (βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)) ↔ βˆ€π‘“ ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏)))
2518, 24bitrdi 286 . . . . . 6 (𝑖 = 𝑑 β†’ (βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)) ↔ βˆ€π‘“ ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏))))
2615, 25anbi12d 631 . . . . 5 (𝑖 = 𝑑 β†’ (((𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))) ↔ ((𝑑 ∈ 𝑏 ∧ Β¬ 𝑑 ∈ 𝑐) ∧ βˆ€π‘“ ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏)))))
2726cbvrexvw 3235 . . . 4 (βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))) ↔ βˆƒπ‘‘ ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑑 ∈ 𝑏 ∧ Β¬ 𝑑 ∈ 𝑐) ∧ βˆ€π‘“ ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏))))
2811, 27bitrdi 286 . . 3 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))) ↔ βˆƒπ‘‘ ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑑 ∈ 𝑏 ∧ Β¬ 𝑑 ∈ 𝑐) ∧ βˆ€π‘“ ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏)))))
2928cbvopabv 5220 . 2 {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))} = {βŸ¨π‘, π‘βŸ© ∣ βˆƒπ‘‘ ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑑 ∈ 𝑏 ∧ Β¬ 𝑑 ∈ 𝑐) ∧ βˆ€π‘“ ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏)))}
30 nfcv 2903 . . 3 Ⅎ𝑐sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})
31 nfcv 2903 . . . 4 Ⅎ𝑔(π‘¦β€˜π‘)
32 nfcv 2903 . . . 4 Ⅎ𝑔(𝑅1β€˜dom 𝑒)
33 nfopab1 5217 . . . 4 Ⅎ𝑔{βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}
3431, 32, 33nfsup 9442 . . 3 Ⅎ𝑔sup((π‘¦β€˜π‘), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})
35 fveq2 6888 . . . 4 (𝑔 = 𝑐 β†’ (π‘¦β€˜π‘”) = (π‘¦β€˜π‘))
3635supeq1d 9437 . . 3 (𝑔 = 𝑐 β†’ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}) = sup((π‘¦β€˜π‘), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))
3730, 34, 36cbvmpt 5258 . 2 (𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})) = (𝑐 ∈ V ↦ sup((π‘¦β€˜π‘), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))
38 nfcv 2903 . . . 4 Ⅎ𝑐((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))
39 nffvmpt1 6899 . . . 4 Ⅎ𝑔((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑐))
40 rneq 5933 . . . . . 6 (𝑔 = 𝑐 β†’ ran 𝑔 = ran 𝑐)
4140difeq2d 4121 . . . . 5 (𝑔 = 𝑐 β†’ ((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔) = ((𝑅1β€˜dom 𝑒) βˆ– ran 𝑐))
4241fveq2d 6892 . . . 4 (𝑔 = 𝑐 β†’ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)) = ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑐)))
4338, 39, 42cbvmpt 5258 . . 3 (𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))) = (𝑐 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑐)))
44 recseq 8370 . . 3 ((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))) = (𝑐 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑐))) β†’ recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) = recs((𝑐 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑐)))))
4543, 44ax-mp 5 . 2 recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) = recs((𝑐 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑐))))
46 nfv 1917 . . 3 β„²π‘βˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž})
47 nfv 1917 . . 3 β„²π‘βˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž})
48 nfmpt1 5255 . . . . . . . 8 Ⅎ𝑔(𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))
4948nfrecs 8371 . . . . . . 7 Ⅎ𝑔recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))))
5049nfcnv 5876 . . . . . 6 Ⅎ𝑔◑recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))))
51 nfcv 2903 . . . . . 6 Ⅎ𝑔{𝑐}
5250, 51nfima 6065 . . . . 5 Ⅎ𝑔(β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐})
5352nfint 4959 . . . 4 β„²π‘”βˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐})
54 nfcv 2903 . . . . . 6 Ⅎ𝑔{𝑏}
5550, 54nfima 6065 . . . . 5 Ⅎ𝑔(β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})
5655nfint 4959 . . . 4 β„²π‘”βˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})
5753, 56nfel 2917 . . 3 β„²π‘”βˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})
58 nfcv 2903 . . . . . . . . 9 β„²β„ŽV
59 nfcv 2903 . . . . . . . . . . . 12 β„²β„Ž(π‘¦β€˜π‘”)
60 nfcv 2903 . . . . . . . . . . . 12 β„²β„Ž(𝑅1β€˜dom 𝑒)
61 nfopab2 5218 . . . . . . . . . . . 12 β„²β„Ž{βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}
6259, 60, 61nfsup 9442 . . . . . . . . . . 11 β„²β„Žsup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})
6358, 62nfmpt 5254 . . . . . . . . . 10 β„²β„Ž(𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))
64 nfcv 2903 . . . . . . . . . 10 β„²β„Ž((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)
6563, 64nffv 6898 . . . . . . . . 9 β„²β„Ž((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))
6658, 65nfmpt 5254 . . . . . . . 8 β„²β„Ž(𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))
6766nfrecs 8371 . . . . . . 7 β„²β„Žrecs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))))
6867nfcnv 5876 . . . . . 6 β„²β„Žβ—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))))
69 nfcv 2903 . . . . . 6 β„²β„Ž{𝑐}
7068, 69nfima 6065 . . . . 5 β„²β„Ž(β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐})
7170nfint 4959 . . . 4 β„²β„Žβˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐})
72 nfcv 2903 . . . . . 6 β„²β„Ž{𝑏}
7368, 72nfima 6065 . . . . 5 β„²β„Ž(β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})
7473nfint 4959 . . . 4 β„²β„Žβˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})
7571, 74nfel 2917 . . 3 β„²β„Žβˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})
76 sneq 4637 . . . . . 6 (𝑔 = 𝑐 β†’ {𝑔} = {𝑐})
7776imaeq2d 6057 . . . . 5 (𝑔 = 𝑐 β†’ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) = (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐}))
7877inteqd 4954 . . . 4 (𝑔 = 𝑐 β†’ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) = ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐}))
79 sneq 4637 . . . . . 6 (β„Ž = 𝑏 β†’ {β„Ž} = {𝑏})
8079imaeq2d 6057 . . . . 5 (β„Ž = 𝑏 β†’ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž}) = (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏}))
8180inteqd 4954 . . . 4 (β„Ž = 𝑏 β†’ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž}) = ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏}))
82 eleq12 2823 . . . 4 ((∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) = ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐}) ∧ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž}) = ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})) β†’ (∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž}) ↔ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})))
8378, 81, 82syl2an 596 . . 3 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž}) ↔ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})))
8446, 47, 57, 75, 83cbvopab 5219 . 2 {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž})} = {βŸ¨π‘, π‘βŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})}
85 fveq2 6888 . . . . 5 (𝑔 = 𝑐 β†’ (rankβ€˜π‘”) = (rankβ€˜π‘))
86 fveq2 6888 . . . . 5 (β„Ž = 𝑏 β†’ (rankβ€˜β„Ž) = (rankβ€˜π‘))
8785, 86breqan12d 5163 . . . 4 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ↔ (rankβ€˜π‘) E (rankβ€˜π‘)))
8885, 86eqeqan12d 2746 . . . . 5 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ↔ (rankβ€˜π‘) = (rankβ€˜π‘)))
89 simpl 483 . . . . . 6 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ 𝑔 = 𝑐)
90 suceq 6427 . . . . . . . . 9 ((rankβ€˜π‘”) = (rankβ€˜π‘) β†’ suc (rankβ€˜π‘”) = suc (rankβ€˜π‘))
9185, 90syl 17 . . . . . . . 8 (𝑔 = 𝑐 β†’ suc (rankβ€˜π‘”) = suc (rankβ€˜π‘))
9291adantr 481 . . . . . . 7 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ suc (rankβ€˜π‘”) = suc (rankβ€˜π‘))
9392fveq2d 6892 . . . . . 6 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (π‘’β€˜suc (rankβ€˜π‘”)) = (π‘’β€˜suc (rankβ€˜π‘)))
94 simpr 485 . . . . . 6 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ β„Ž = 𝑏)
9589, 93, 94breq123d 5161 . . . . 5 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž ↔ 𝑐(π‘’β€˜suc (rankβ€˜π‘))𝑏))
9688, 95anbi12d 631 . . . 4 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž) ↔ ((rankβ€˜π‘) = (rankβ€˜π‘) ∧ 𝑐(π‘’β€˜suc (rankβ€˜π‘))𝑏)))
9787, 96orbi12d 917 . . 3 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž)) ↔ ((rankβ€˜π‘) E (rankβ€˜π‘) ∨ ((rankβ€˜π‘) = (rankβ€˜π‘) ∧ 𝑐(π‘’β€˜suc (rankβ€˜π‘))𝑏))))
9897cbvopabv 5220 . 2 {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))} = {βŸ¨π‘, π‘βŸ© ∣ ((rankβ€˜π‘) E (rankβ€˜π‘) ∨ ((rankβ€˜π‘) = (rankβ€˜π‘) ∧ 𝑐(π‘’β€˜suc (rankβ€˜π‘))𝑏))}
99 eqid 2732 . 2 (if(dom 𝑒 = βˆͺ dom 𝑒, {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))}, {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž})}) ∩ ((𝑅1β€˜dom 𝑒) Γ— (𝑅1β€˜dom 𝑒))) = (if(dom 𝑒 = βˆͺ dom 𝑒, {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))}, {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž})}) ∩ ((𝑅1β€˜dom 𝑒) Γ— (𝑅1β€˜dom 𝑒)))
100 dmeq 5901 . . . . . . 7 (𝑙 = 𝑒 β†’ dom 𝑙 = dom 𝑒)
101100unieqd 4921 . . . . . . 7 (𝑙 = 𝑒 β†’ βˆͺ dom 𝑙 = βˆͺ dom 𝑒)
102100, 101eqeq12d 2748 . . . . . 6 (𝑙 = 𝑒 β†’ (dom 𝑙 = βˆͺ dom 𝑙 ↔ dom 𝑒 = βˆͺ dom 𝑒))
103 fveq1 6887 . . . . . . . . . 10 (𝑙 = 𝑒 β†’ (π‘™β€˜suc (rankβ€˜π‘”)) = (π‘’β€˜suc (rankβ€˜π‘”)))
104103breqd 5158 . . . . . . . . 9 (𝑙 = 𝑒 β†’ (𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž ↔ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))
105104anbi2d 629 . . . . . . . 8 (𝑙 = 𝑒 β†’ (((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž) ↔ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž)))
106105orbi2d 914 . . . . . . 7 (𝑙 = 𝑒 β†’ (((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž)) ↔ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))))
107106opabbidv 5213 . . . . . 6 (𝑙 = 𝑒 β†’ {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž))} = {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))})
108 eqidd 2733 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑒 β†’ (π‘¦β€˜π‘”) = (π‘¦β€˜π‘”))
109100fveq2d 6892 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑒 β†’ (𝑅1β€˜dom 𝑙) = (𝑅1β€˜dom 𝑒))
110101fveq2d 6892 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑒 β†’ (𝑅1β€˜βˆͺ dom 𝑙) = (𝑅1β€˜βˆͺ dom 𝑒))
111 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = 𝑒 β†’ 𝑙 = 𝑒)
112111, 101fveq12d 6895 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 = 𝑒 β†’ (π‘™β€˜βˆͺ dom 𝑙) = (π‘’β€˜βˆͺ dom 𝑒))
113112breqd 5158 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑒 β†’ (𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 ↔ 𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖))
114113imbi1d 341 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑒 β†’ ((𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)) ↔ (𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))))
115110, 114raleqbidv 3342 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑒 β†’ (βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)) ↔ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))))
116115anbi2d 629 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑒 β†’ (((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))) ↔ ((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))))
117110, 116rexeqbidv 3343 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑒 β†’ (βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))) ↔ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))))
118117opabbidv 5213 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑒 β†’ {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))} = {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})
119108, 109, 118supeq123d 9441 . . . . . . . . . . . . . . 15 (𝑙 = 𝑒 β†’ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}) = sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))
120119mpteq2dv 5249 . . . . . . . . . . . . . 14 (𝑙 = 𝑒 β†’ (𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})) = (𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})))
121109difeq1d 4120 . . . . . . . . . . . . . 14 (𝑙 = 𝑒 β†’ ((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔) = ((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))
122120, 121fveq12d 6895 . . . . . . . . . . . . 13 (𝑙 = 𝑒 β†’ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)) = ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))
123122mpteq2dv 5249 . . . . . . . . . . . 12 (𝑙 = 𝑒 β†’ (𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔))) = (𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))))
124 recseq 8370 . . . . . . . . . . . 12 ((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔))) = (𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))) β†’ recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) = recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))))
125123, 124syl 17 . . . . . . . . . . 11 (𝑙 = 𝑒 β†’ recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) = recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))))
126125cnveqd 5873 . . . . . . . . . 10 (𝑙 = 𝑒 β†’ β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) = β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))))
127126imaeq1d 6056 . . . . . . . . 9 (𝑙 = 𝑒 β†’ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {𝑔}) = (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}))
128127inteqd 4954 . . . . . . . 8 (𝑙 = 𝑒 β†’ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {𝑔}) = ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}))
129126imaeq1d 6056 . . . . . . . . 9 (𝑙 = 𝑒 β†’ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {β„Ž}) = (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž}))
130129inteqd 4954 . . . . . . . 8 (𝑙 = 𝑒 β†’ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {β„Ž}) = ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž}))
131128, 130eleq12d 2827 . . . . . . 7 (𝑙 = 𝑒 β†’ (∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {β„Ž}) ↔ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž})))
132131opabbidv 5213 . . . . . 6 (𝑙 = 𝑒 β†’ {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {β„Ž})} = {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž})})
133102, 107, 132ifbieq12d 4555 . . . . 5 (𝑙 = 𝑒 β†’ if(dom 𝑙 = βˆͺ dom 𝑙, {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž))}, {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {β„Ž})}) = if(dom 𝑒 = βˆͺ dom 𝑒, {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))}, {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž})}))
134109sqxpeqd 5707 . . . . 5 (𝑙 = 𝑒 β†’ ((𝑅1β€˜dom 𝑙) Γ— (𝑅1β€˜dom 𝑙)) = ((𝑅1β€˜dom 𝑒) Γ— (𝑅1β€˜dom 𝑒)))
135133, 134ineq12d 4212 . . . 4 (𝑙 = 𝑒 β†’ (if(dom 𝑙 = βˆͺ dom 𝑙, {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž))}, {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {β„Ž})}) ∩ ((𝑅1β€˜dom 𝑙) Γ— (𝑅1β€˜dom 𝑙))) = (if(dom 𝑒 = βˆͺ dom 𝑒, {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))}, {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž})}) ∩ ((𝑅1β€˜dom 𝑒) Γ— (𝑅1β€˜dom 𝑒))))
136135cbvmptv 5260 . . 3 (𝑙 ∈ V ↦ (if(dom 𝑙 = βˆͺ dom 𝑙, {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž))}, {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {β„Ž})}) ∩ ((𝑅1β€˜dom 𝑙) Γ— (𝑅1β€˜dom 𝑙)))) = (𝑒 ∈ V ↦ (if(dom 𝑒 = βˆͺ dom 𝑒, {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))}, {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž})}) ∩ ((𝑅1β€˜dom 𝑒) Γ— (𝑅1β€˜dom 𝑒))))
137 recseq 8370 . . 3 ((𝑙 ∈ V ↦ (if(dom 𝑙 = βˆͺ dom 𝑙, {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž))}, {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {β„Ž})}) ∩ ((𝑅1β€˜dom 𝑙) Γ— (𝑅1β€˜dom 𝑙)))) = (𝑒 ∈ V ↦ (if(dom 𝑒 = βˆͺ dom 𝑒, {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))}, {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž})}) ∩ ((𝑅1β€˜dom 𝑒) Γ— (𝑅1β€˜dom 𝑒)))) β†’ recs((𝑙 ∈ V ↦ (if(dom 𝑙 = βˆͺ dom 𝑙, {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž))}, {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {β„Ž})}) ∩ ((𝑅1β€˜dom 𝑙) Γ— (𝑅1β€˜dom 𝑙))))) = recs((𝑒 ∈ V ↦ (if(dom 𝑒 = βˆͺ dom 𝑒, {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))}, {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž})}) ∩ ((𝑅1β€˜dom 𝑒) Γ— (𝑅1β€˜dom 𝑒))))))
138136, 137ax-mp 5 . 2 recs((𝑙 ∈ V ↦ (if(dom 𝑙 = βˆͺ dom 𝑙, {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž))}, {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔)))) β€œ {β„Ž})}) ∩ ((𝑅1β€˜dom 𝑙) Γ— (𝑅1β€˜dom 𝑙))))) = recs((𝑒 ∈ V ↦ (if(dom 𝑒 = βˆͺ dom 𝑒, {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))}, {βŸ¨π‘”, β„ŽβŸ© ∣ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑔}) ∈ ∩ (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {β„Ž})}) ∩ ((𝑅1β€˜dom 𝑒) Γ— (𝑅1β€˜dom 𝑒)))))
139 aomclem8.a . 2 (πœ‘ β†’ 𝐴 ∈ On)
140 aomclem8.y . . 3 (πœ‘ β†’ βˆ€π‘Ž ∈ 𝒫 (𝑅1β€˜π΄)(π‘Ž β‰  βˆ… β†’ (π‘¦β€˜π‘Ž) ∈ ((𝒫 π‘Ž ∩ Fin) βˆ– {βˆ…})))
141 neeq1 3003 . . . . 5 (π‘Ž = 𝑐 β†’ (π‘Ž β‰  βˆ… ↔ 𝑐 β‰  βˆ…))
142 fveq2 6888 . . . . . 6 (π‘Ž = 𝑐 β†’ (π‘¦β€˜π‘Ž) = (π‘¦β€˜π‘))
143 pweq 4615 . . . . . . . 8 (π‘Ž = 𝑐 β†’ 𝒫 π‘Ž = 𝒫 𝑐)
144143ineq1d 4210 . . . . . . 7 (π‘Ž = 𝑐 β†’ (𝒫 π‘Ž ∩ Fin) = (𝒫 𝑐 ∩ Fin))
145144difeq1d 4120 . . . . . 6 (π‘Ž = 𝑐 β†’ ((𝒫 π‘Ž ∩ Fin) βˆ– {βˆ…}) = ((𝒫 𝑐 ∩ Fin) βˆ– {βˆ…}))
146142, 145eleq12d 2827 . . . . 5 (π‘Ž = 𝑐 β†’ ((π‘¦β€˜π‘Ž) ∈ ((𝒫 π‘Ž ∩ Fin) βˆ– {βˆ…}) ↔ (π‘¦β€˜π‘) ∈ ((𝒫 𝑐 ∩ Fin) βˆ– {βˆ…})))
147141, 146imbi12d 344 . . . 4 (π‘Ž = 𝑐 β†’ ((π‘Ž β‰  βˆ… β†’ (π‘¦β€˜π‘Ž) ∈ ((𝒫 π‘Ž ∩ Fin) βˆ– {βˆ…})) ↔ (𝑐 β‰  βˆ… β†’ (π‘¦β€˜π‘) ∈ ((𝒫 𝑐 ∩ Fin) βˆ– {βˆ…}))))
148147cbvralvw 3234 . . 3 (βˆ€π‘Ž ∈ 𝒫 (𝑅1β€˜π΄)(π‘Ž β‰  βˆ… β†’ (π‘¦β€˜π‘Ž) ∈ ((𝒫 π‘Ž ∩ Fin) βˆ– {βˆ…})) ↔ βˆ€π‘ ∈ 𝒫 (𝑅1β€˜π΄)(𝑐 β‰  βˆ… β†’ (π‘¦β€˜π‘) ∈ ((𝒫 𝑐 ∩ Fin) βˆ– {βˆ…})))
149140, 148sylib 217 . 2 (πœ‘ β†’ βˆ€π‘ ∈ 𝒫 (𝑅1β€˜π΄)(𝑐 β‰  βˆ… β†’ (π‘¦β€˜π‘) ∈ ((𝒫 𝑐 ∩ Fin) βˆ– {βˆ…})))
15029, 37, 45, 84, 98, 99, 138, 139, 149aomclem7 41787 1 (πœ‘ β†’ βˆƒπ‘ 𝑏 We (𝑅1β€˜π΄))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3474   βˆ– cdif 3944   ∩ cin 3946  βˆ…c0 4321  ifcif 4527  π’« cpw 4601  {csn 4627  βˆͺ cuni 4907  βˆ© cint 4949   class class class wbr 5147  {copab 5209   ↦ cmpt 5230   E cep 5578   We wwe 5629   Γ— cxp 5673  β—‘ccnv 5674  dom cdm 5675  ran crn 5676   β€œ cima 5678  Oncon0 6361  suc csuc 6363  β€˜cfv 6540  recscrecs 8366  Fincfn 8935  supcsup 9431  π‘…1cr1 9753  rankcrnk 9754
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-map 8818  df-en 8936  df-fin 8939  df-sup 9433  df-r1 9755  df-rank 9756
This theorem is referenced by:  dfac11  41789
  Copyright terms: Public domain W3C validator