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 41417
Description: Lemma for dfac11 41418. 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 2122 . . . . . . 7 (β„Ž = 𝑏 β†’ (𝑖 ∈ β„Ž ↔ 𝑖 ∈ 𝑏))
2 elequ2 2122 . . . . . . . 8 (𝑔 = 𝑐 β†’ (𝑖 ∈ 𝑔 ↔ 𝑖 ∈ 𝑐))
32notbid 318 . . . . . . 7 (𝑔 = 𝑐 β†’ (Β¬ 𝑖 ∈ 𝑔 ↔ Β¬ 𝑖 ∈ 𝑐))
41, 3bi2anan9r 639 . . . . . 6 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ ((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ↔ (𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐)))
5 elequ2 2122 . . . . . . . . 9 (𝑔 = 𝑐 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ 𝑐))
6 elequ2 2122 . . . . . . . . 9 (β„Ž = 𝑏 β†’ (𝑗 ∈ β„Ž ↔ 𝑗 ∈ 𝑏))
75, 6bi2bian9 640 . . . . . . . 8 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ ((𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž) ↔ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)))
87imbi2d 341 . . . . . . 7 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ ((𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)) ↔ (𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))))
98ralbidv 3175 . . . . . 6 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)) ↔ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))))
104, 9anbi12d 632 . . . . 5 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))) ↔ ((𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)))))
1110rexbidv 3176 . . . 4 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))) ↔ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)))))
12 elequ1 2114 . . . . . . 7 (𝑖 = 𝑑 β†’ (𝑖 ∈ 𝑏 ↔ 𝑑 ∈ 𝑏))
13 elequ1 2114 . . . . . . . 8 (𝑖 = 𝑑 β†’ (𝑖 ∈ 𝑐 ↔ 𝑑 ∈ 𝑐))
1413notbid 318 . . . . . . 7 (𝑖 = 𝑑 β†’ (Β¬ 𝑖 ∈ 𝑐 ↔ Β¬ 𝑑 ∈ 𝑐))
1512, 14anbi12d 632 . . . . . 6 (𝑖 = 𝑑 β†’ ((𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐) ↔ (𝑑 ∈ 𝑏 ∧ Β¬ 𝑑 ∈ 𝑐)))
16 breq2 5114 . . . . . . . . 9 (𝑖 = 𝑑 β†’ (𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 ↔ 𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑))
1716imbi1d 342 . . . . . . . 8 (𝑖 = 𝑑 β†’ ((𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)) ↔ (𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))))
1817ralbidv 3175 . . . . . . 7 (𝑖 = 𝑑 β†’ (βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)) ↔ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))))
19 breq1 5113 . . . . . . . . 9 (𝑗 = 𝑓 β†’ (𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑 ↔ 𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑))
20 elequ1 2114 . . . . . . . . . 10 (𝑗 = 𝑓 β†’ (𝑗 ∈ 𝑐 ↔ 𝑓 ∈ 𝑐))
21 elequ1 2114 . . . . . . . . . 10 (𝑗 = 𝑓 β†’ (𝑗 ∈ 𝑏 ↔ 𝑓 ∈ 𝑏))
2220, 21bibi12d 346 . . . . . . . . 9 (𝑗 = 𝑓 β†’ ((𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏) ↔ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏)))
2319, 22imbi12d 345 . . . . . . . 8 (𝑗 = 𝑓 β†’ ((𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)) ↔ (𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏))))
2423cbvralvw 3228 . . . . . . 7 (βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)) ↔ βˆ€π‘“ ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏)))
2518, 24bitrdi 287 . . . . . 6 (𝑖 = 𝑑 β†’ (βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)) ↔ βˆ€π‘“ ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏))))
2615, 25anbi12d 632 . . . . 5 (𝑖 = 𝑑 β†’ (((𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))) ↔ ((𝑑 ∈ 𝑏 ∧ Β¬ 𝑑 ∈ 𝑐) ∧ βˆ€π‘“ ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏)))))
2726cbvrexvw 3229 . . . 4 (βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))) ↔ βˆƒπ‘‘ ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑑 ∈ 𝑏 ∧ Β¬ 𝑑 ∈ 𝑐) ∧ βˆ€π‘“ ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏))))
2811, 27bitrdi 287 . . 3 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))) ↔ βˆƒπ‘‘ ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑑 ∈ 𝑏 ∧ Β¬ 𝑑 ∈ 𝑐) ∧ βˆ€π‘“ ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏)))))
2928cbvopabv 5183 . 2 {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))} = {βŸ¨π‘, π‘βŸ© ∣ βˆƒπ‘‘ ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑑 ∈ 𝑏 ∧ Β¬ 𝑑 ∈ 𝑐) ∧ βˆ€π‘“ ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏)))}
30 nfcv 2908 . . 3 Ⅎ𝑐sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})
31 nfcv 2908 . . . 4 Ⅎ𝑔(π‘¦β€˜π‘)
32 nfcv 2908 . . . 4 Ⅎ𝑔(𝑅1β€˜dom 𝑒)
33 nfopab1 5180 . . . 4 Ⅎ𝑔{βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}
3431, 32, 33nfsup 9394 . . 3 Ⅎ𝑔sup((π‘¦β€˜π‘), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})
35 fveq2 6847 . . . 4 (𝑔 = 𝑐 β†’ (π‘¦β€˜π‘”) = (π‘¦β€˜π‘))
3635supeq1d 9389 . . 3 (𝑔 = 𝑐 β†’ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}) = sup((π‘¦β€˜π‘), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))
3730, 34, 36cbvmpt 5221 . 2 (𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})) = (𝑐 ∈ V ↦ sup((π‘¦β€˜π‘), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))
38 nfcv 2908 . . . 4 Ⅎ𝑐((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))
39 nffvmpt1 6858 . . . 4 Ⅎ𝑔((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑐))
40 rneq 5896 . . . . . 6 (𝑔 = 𝑐 β†’ ran 𝑔 = ran 𝑐)
4140difeq2d 4087 . . . . 5 (𝑔 = 𝑐 β†’ ((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔) = ((𝑅1β€˜dom 𝑒) βˆ– ran 𝑐))
4241fveq2d 6851 . . . 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 5221 . . 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 8325 . . 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 1918 . . 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 1918 . . 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 5218 . . . . . . . 8 Ⅎ𝑔(𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))
4948nfrecs 8326 . . . . . . 7 Ⅎ𝑔recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))))
5049nfcnv 5839 . . . . . 6 Ⅎ𝑔◑recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))))
51 nfcv 2908 . . . . . 6 Ⅎ𝑔{𝑐}
5250, 51nfima 6026 . . . . 5 Ⅎ𝑔(β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐})
5352nfint 4922 . . . 4 β„²π‘”βˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐})
54 nfcv 2908 . . . . . 6 Ⅎ𝑔{𝑏}
5550, 54nfima 6026 . . . . 5 Ⅎ𝑔(β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})
5655nfint 4922 . . . 4 β„²π‘”βˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})
5753, 56nfel 2922 . . 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 2908 . . . . . . . . 9 β„²β„ŽV
59 nfcv 2908 . . . . . . . . . . . 12 β„²β„Ž(π‘¦β€˜π‘”)
60 nfcv 2908 . . . . . . . . . . . 12 β„²β„Ž(𝑅1β€˜dom 𝑒)
61 nfopab2 5181 . . . . . . . . . . . 12 β„²β„Ž{βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}
6259, 60, 61nfsup 9394 . . . . . . . . . . 11 β„²β„Žsup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})
6358, 62nfmpt 5217 . . . . . . . . . 10 β„²β„Ž(𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))
64 nfcv 2908 . . . . . . . . . 10 β„²β„Ž((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)
6563, 64nffv 6857 . . . . . . . . 9 β„²β„Ž((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))
6658, 65nfmpt 5217 . . . . . . . 8 β„²β„Ž(𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))
6766nfrecs 8326 . . . . . . 7 β„²β„Žrecs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))))
6867nfcnv 5839 . . . . . 6 β„²β„Žβ—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))))
69 nfcv 2908 . . . . . 6 β„²β„Ž{𝑐}
7068, 69nfima 6026 . . . . 5 β„²β„Ž(β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐})
7170nfint 4922 . . . 4 β„²β„Žβˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐})
72 nfcv 2908 . . . . . 6 β„²β„Ž{𝑏}
7368, 72nfima 6026 . . . . 5 β„²β„Ž(β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})
7473nfint 4922 . . . 4 β„²β„Žβˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})
7571, 74nfel 2922 . . 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 4601 . . . . . 6 (𝑔 = 𝑐 β†’ {𝑔} = {𝑐})
7776imaeq2d 6018 . . . . 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 4917 . . . 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 4601 . . . . . 6 (β„Ž = 𝑏 β†’ {β„Ž} = {𝑏})
8079imaeq2d 6018 . . . . 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 4917 . . . 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 2828 . . . 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 597 . . 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 5182 . 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 6847 . . . . 5 (𝑔 = 𝑐 β†’ (rankβ€˜π‘”) = (rankβ€˜π‘))
86 fveq2 6847 . . . . 5 (β„Ž = 𝑏 β†’ (rankβ€˜β„Ž) = (rankβ€˜π‘))
8785, 86breqan12d 5126 . . . 4 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ↔ (rankβ€˜π‘) E (rankβ€˜π‘)))
8885, 86eqeqan12d 2751 . . . . 5 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ↔ (rankβ€˜π‘) = (rankβ€˜π‘)))
89 simpl 484 . . . . . 6 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ 𝑔 = 𝑐)
90 suceq 6388 . . . . . . . . 9 ((rankβ€˜π‘”) = (rankβ€˜π‘) β†’ suc (rankβ€˜π‘”) = suc (rankβ€˜π‘))
9185, 90syl 17 . . . . . . . 8 (𝑔 = 𝑐 β†’ suc (rankβ€˜π‘”) = suc (rankβ€˜π‘))
9291adantr 482 . . . . . . 7 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ suc (rankβ€˜π‘”) = suc (rankβ€˜π‘))
9392fveq2d 6851 . . . . . 6 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (π‘’β€˜suc (rankβ€˜π‘”)) = (π‘’β€˜suc (rankβ€˜π‘)))
94 simpr 486 . . . . . 6 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ β„Ž = 𝑏)
9589, 93, 94breq123d 5124 . . . . 5 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž ↔ 𝑐(π‘’β€˜suc (rankβ€˜π‘))𝑏))
9688, 95anbi12d 632 . . . 4 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž) ↔ ((rankβ€˜π‘) = (rankβ€˜π‘) ∧ 𝑐(π‘’β€˜suc (rankβ€˜π‘))𝑏)))
9787, 96orbi12d 918 . . 3 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž)) ↔ ((rankβ€˜π‘) E (rankβ€˜π‘) ∨ ((rankβ€˜π‘) = (rankβ€˜π‘) ∧ 𝑐(π‘’β€˜suc (rankβ€˜π‘))𝑏))))
9897cbvopabv 5183 . 2 {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))} = {βŸ¨π‘, π‘βŸ© ∣ ((rankβ€˜π‘) E (rankβ€˜π‘) ∨ ((rankβ€˜π‘) = (rankβ€˜π‘) ∧ 𝑐(π‘’β€˜suc (rankβ€˜π‘))𝑏))}
99 eqid 2737 . 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 5864 . . . . . . 7 (𝑙 = 𝑒 β†’ dom 𝑙 = dom 𝑒)
101100unieqd 4884 . . . . . . 7 (𝑙 = 𝑒 β†’ βˆͺ dom 𝑙 = βˆͺ dom 𝑒)
102100, 101eqeq12d 2753 . . . . . 6 (𝑙 = 𝑒 β†’ (dom 𝑙 = βˆͺ dom 𝑙 ↔ dom 𝑒 = βˆͺ dom 𝑒))
103 fveq1 6846 . . . . . . . . . 10 (𝑙 = 𝑒 β†’ (π‘™β€˜suc (rankβ€˜π‘”)) = (π‘’β€˜suc (rankβ€˜π‘”)))
104103breqd 5121 . . . . . . . . 9 (𝑙 = 𝑒 β†’ (𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž ↔ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))
105104anbi2d 630 . . . . . . . 8 (𝑙 = 𝑒 β†’ (((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž) ↔ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž)))
106105orbi2d 915 . . . . . . 7 (𝑙 = 𝑒 β†’ (((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž)) ↔ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))))
107106opabbidv 5176 . . . . . 6 (𝑙 = 𝑒 β†’ {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž))} = {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))})
108 eqidd 2738 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑒 β†’ (π‘¦β€˜π‘”) = (π‘¦β€˜π‘”))
109100fveq2d 6851 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑒 β†’ (𝑅1β€˜dom 𝑙) = (𝑅1β€˜dom 𝑒))
110101fveq2d 6851 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑒 β†’ (𝑅1β€˜βˆͺ dom 𝑙) = (𝑅1β€˜βˆͺ dom 𝑒))
111 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = 𝑒 β†’ 𝑙 = 𝑒)
112111, 101fveq12d 6854 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 = 𝑒 β†’ (π‘™β€˜βˆͺ dom 𝑙) = (π‘’β€˜βˆͺ dom 𝑒))
113112breqd 5121 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑒 β†’ (𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 ↔ 𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖))
114113imbi1d 342 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑒 β†’ ((𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)) ↔ (𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))))
115110, 114raleqbidv 3322 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑒 β†’ (βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)) ↔ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))))
116115anbi2d 630 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑒 β†’ (((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))) ↔ ((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))))
117110, 116rexeqbidv 3323 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑒 β†’ (βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))) ↔ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))))
118117opabbidv 5176 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑒 β†’ {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))} = {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})
119108, 109, 118supeq123d 9393 . . . . . . . . . . . . . . 15 (𝑙 = 𝑒 β†’ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}) = sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))
120119mpteq2dv 5212 . . . . . . . . . . . . . 14 (𝑙 = 𝑒 β†’ (𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})) = (𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})))
121109difeq1d 4086 . . . . . . . . . . . . . 14 (𝑙 = 𝑒 β†’ ((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔) = ((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))
122120, 121fveq12d 6854 . . . . . . . . . . . . 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 5212 . . . . . . . . . . . 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 8325 . . . . . . . . . . . 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 5836 . . . . . . . . . 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 6017 . . . . . . . . 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 4917 . . . . . . . 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 6017 . . . . . . . . 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 4917 . . . . . . . 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 2832 . . . . . . 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 5176 . . . . . 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 4519 . . . . 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 5670 . . . . 5 (𝑙 = 𝑒 β†’ ((𝑅1β€˜dom 𝑙) Γ— (𝑅1β€˜dom 𝑙)) = ((𝑅1β€˜dom 𝑒) Γ— (𝑅1β€˜dom 𝑒)))
135133, 134ineq12d 4178 . . . 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 5223 . . 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 8325 . . 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 3007 . . . . 5 (π‘Ž = 𝑐 β†’ (π‘Ž β‰  βˆ… ↔ 𝑐 β‰  βˆ…))
142 fveq2 6847 . . . . . 6 (π‘Ž = 𝑐 β†’ (π‘¦β€˜π‘Ž) = (π‘¦β€˜π‘))
143 pweq 4579 . . . . . . . 8 (π‘Ž = 𝑐 β†’ 𝒫 π‘Ž = 𝒫 𝑐)
144143ineq1d 4176 . . . . . . 7 (π‘Ž = 𝑐 β†’ (𝒫 π‘Ž ∩ Fin) = (𝒫 𝑐 ∩ Fin))
145144difeq1d 4086 . . . . . 6 (π‘Ž = 𝑐 β†’ ((𝒫 π‘Ž ∩ Fin) βˆ– {βˆ…}) = ((𝒫 𝑐 ∩ Fin) βˆ– {βˆ…}))
146142, 145eleq12d 2832 . . . . 5 (π‘Ž = 𝑐 β†’ ((π‘¦β€˜π‘Ž) ∈ ((𝒫 π‘Ž ∩ Fin) βˆ– {βˆ…}) ↔ (π‘¦β€˜π‘) ∈ ((𝒫 𝑐 ∩ Fin) βˆ– {βˆ…})))
147141, 146imbi12d 345 . . . 4 (π‘Ž = 𝑐 β†’ ((π‘Ž β‰  βˆ… β†’ (π‘¦β€˜π‘Ž) ∈ ((𝒫 π‘Ž ∩ Fin) βˆ– {βˆ…})) ↔ (𝑐 β‰  βˆ… β†’ (π‘¦β€˜π‘) ∈ ((𝒫 𝑐 ∩ Fin) βˆ– {βˆ…}))))
148147cbvralvw 3228 . . 3 (βˆ€π‘Ž ∈ 𝒫 (𝑅1β€˜π΄)(π‘Ž β‰  βˆ… β†’ (π‘¦β€˜π‘Ž) ∈ ((𝒫 π‘Ž ∩ Fin) βˆ– {βˆ…})) ↔ βˆ€π‘ ∈ 𝒫 (𝑅1β€˜π΄)(𝑐 β‰  βˆ… β†’ (π‘¦β€˜π‘) ∈ ((𝒫 𝑐 ∩ Fin) βˆ– {βˆ…})))
149140, 148sylib 217 . 2 (πœ‘ β†’ βˆ€π‘ ∈ 𝒫 (𝑅1β€˜π΄)(𝑐 β‰  βˆ… β†’ (π‘¦β€˜π‘) ∈ ((𝒫 𝑐 ∩ Fin) βˆ– {βˆ…})))
15029, 37, 45, 84, 98, 99, 138, 139, 149aomclem7 41416 1 (πœ‘ β†’ βˆƒπ‘ 𝑏 We (𝑅1β€˜π΄))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  Vcvv 3448   βˆ– cdif 3912   ∩ cin 3914  βˆ…c0 4287  ifcif 4491  π’« cpw 4565  {csn 4591  βˆͺ cuni 4870  βˆ© cint 4912   class class class wbr 5110  {copab 5172   ↦ cmpt 5193   E cep 5541   We wwe 5592   Γ— cxp 5636  β—‘ccnv 5637  dom cdm 5638  ran crn 5639   β€œ cima 5641  Oncon0 6322  suc csuc 6324  β€˜cfv 6501  recscrecs 8321  Fincfn 8890  supcsup 9383  π‘…1cr1 9705  rankcrnk 9706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-map 8774  df-en 8891  df-fin 8894  df-sup 9385  df-r1 9707  df-rank 9708
This theorem is referenced by:  dfac11  41418
  Copyright terms: Public domain W3C validator