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 42381
Description: Lemma for dfac11 42382. 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 2113 . . . . . . 7 (β„Ž = 𝑏 β†’ (𝑖 ∈ β„Ž ↔ 𝑖 ∈ 𝑏))
2 elequ2 2113 . . . . . . . 8 (𝑔 = 𝑐 β†’ (𝑖 ∈ 𝑔 ↔ 𝑖 ∈ 𝑐))
32notbid 318 . . . . . . 7 (𝑔 = 𝑐 β†’ (Β¬ 𝑖 ∈ 𝑔 ↔ Β¬ 𝑖 ∈ 𝑐))
41, 3bi2anan9r 637 . . . . . 6 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ ((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ↔ (𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐)))
5 elequ2 2113 . . . . . . . . 9 (𝑔 = 𝑐 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ 𝑐))
6 elequ2 2113 . . . . . . . . 9 (β„Ž = 𝑏 β†’ (𝑗 ∈ β„Ž ↔ 𝑗 ∈ 𝑏))
75, 6bi2bian9 638 . . . . . . . 8 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ ((𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž) ↔ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)))
87imbi2d 340 . . . . . . 7 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ ((𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)) ↔ (𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))))
98ralbidv 3171 . . . . . 6 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)) ↔ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))))
104, 9anbi12d 630 . . . . 5 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))) ↔ ((𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)))))
1110rexbidv 3172 . . . 4 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))) ↔ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)))))
12 elequ1 2105 . . . . . . 7 (𝑖 = 𝑑 β†’ (𝑖 ∈ 𝑏 ↔ 𝑑 ∈ 𝑏))
13 elequ1 2105 . . . . . . . 8 (𝑖 = 𝑑 β†’ (𝑖 ∈ 𝑐 ↔ 𝑑 ∈ 𝑐))
1413notbid 318 . . . . . . 7 (𝑖 = 𝑑 β†’ (Β¬ 𝑖 ∈ 𝑐 ↔ Β¬ 𝑑 ∈ 𝑐))
1512, 14anbi12d 630 . . . . . 6 (𝑖 = 𝑑 β†’ ((𝑖 ∈ 𝑏 ∧ Β¬ 𝑖 ∈ 𝑐) ↔ (𝑑 ∈ 𝑏 ∧ Β¬ 𝑑 ∈ 𝑐)))
16 breq2 5145 . . . . . . . . 9 (𝑖 = 𝑑 β†’ (𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 ↔ 𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑))
1716imbi1d 341 . . . . . . . 8 (𝑖 = 𝑑 β†’ ((𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)) ↔ (𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))))
1817ralbidv 3171 . . . . . . 7 (𝑖 = 𝑑 β†’ (βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)) ↔ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏))))
19 breq1 5144 . . . . . . . . 9 (𝑗 = 𝑓 β†’ (𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑 ↔ 𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑))
20 elequ1 2105 . . . . . . . . . 10 (𝑗 = 𝑓 β†’ (𝑗 ∈ 𝑐 ↔ 𝑓 ∈ 𝑐))
21 elequ1 2105 . . . . . . . . . 10 (𝑗 = 𝑓 β†’ (𝑗 ∈ 𝑏 ↔ 𝑓 ∈ 𝑏))
2220, 21bibi12d 345 . . . . . . . . 9 (𝑗 = 𝑓 β†’ ((𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏) ↔ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏)))
2319, 22imbi12d 344 . . . . . . . 8 (𝑗 = 𝑓 β†’ ((𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)) ↔ (𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏))))
2423cbvralvw 3228 . . . . . . 7 (βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)) ↔ βˆ€π‘“ ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏)))
2518, 24bitrdi 287 . . . . . 6 (𝑖 = 𝑑 β†’ (βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏)) ↔ βˆ€π‘“ ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏))))
2615, 25anbi12d 630 . . . . 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 5214 . 2 {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))} = {βŸ¨π‘, π‘βŸ© ∣ βˆƒπ‘‘ ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑑 ∈ 𝑏 ∧ Β¬ 𝑑 ∈ 𝑐) ∧ βˆ€π‘“ ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑓(π‘’β€˜βˆͺ dom 𝑒)𝑑 β†’ (𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏)))}
30 nfcv 2897 . . 3 Ⅎ𝑐sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})
31 nfcv 2897 . . . 4 Ⅎ𝑔(π‘¦β€˜π‘)
32 nfcv 2897 . . . 4 Ⅎ𝑔(𝑅1β€˜dom 𝑒)
33 nfopab1 5211 . . . 4 Ⅎ𝑔{βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}
3431, 32, 33nfsup 9448 . . 3 Ⅎ𝑔sup((π‘¦β€˜π‘), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})
35 fveq2 6885 . . . 4 (𝑔 = 𝑐 β†’ (π‘¦β€˜π‘”) = (π‘¦β€˜π‘))
3635supeq1d 9443 . . 3 (𝑔 = 𝑐 β†’ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}) = sup((π‘¦β€˜π‘), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))
3730, 34, 36cbvmpt 5252 . 2 (𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})) = (𝑐 ∈ V ↦ sup((π‘¦β€˜π‘), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))
38 nfcv 2897 . . . 4 Ⅎ𝑐((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))
39 nffvmpt1 6896 . . . 4 Ⅎ𝑔((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑐))
40 rneq 5929 . . . . . 6 (𝑔 = 𝑐 β†’ ran 𝑔 = ran 𝑐)
4140difeq2d 4117 . . . . 5 (𝑔 = 𝑐 β†’ ((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔) = ((𝑅1β€˜dom 𝑒) βˆ– ran 𝑐))
4241fveq2d 6889 . . . 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 5252 . . 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 8375 . . 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 1909 . . 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 1909 . . 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 5249 . . . . . . . 8 Ⅎ𝑔(𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))
4948nfrecs 8376 . . . . . . 7 Ⅎ𝑔recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))))
5049nfcnv 5872 . . . . . 6 Ⅎ𝑔◑recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))))
51 nfcv 2897 . . . . . 6 Ⅎ𝑔{𝑐}
5250, 51nfima 6061 . . . . 5 Ⅎ𝑔(β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐})
5352nfint 4953 . . . 4 β„²π‘”βˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐})
54 nfcv 2897 . . . . . 6 Ⅎ𝑔{𝑏}
5550, 54nfima 6061 . . . . 5 Ⅎ𝑔(β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})
5655nfint 4953 . . . 4 β„²π‘”βˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})
5753, 56nfel 2911 . . 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 2897 . . . . . . . . 9 β„²β„ŽV
59 nfcv 2897 . . . . . . . . . . . 12 β„²β„Ž(π‘¦β€˜π‘”)
60 nfcv 2897 . . . . . . . . . . . 12 β„²β„Ž(𝑅1β€˜dom 𝑒)
61 nfopab2 5212 . . . . . . . . . . . 12 β„²β„Ž{βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}
6259, 60, 61nfsup 9448 . . . . . . . . . . 11 β„²β„Žsup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})
6358, 62nfmpt 5248 . . . . . . . . . 10 β„²β„Ž(𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))
64 nfcv 2897 . . . . . . . . . 10 β„²β„Ž((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)
6563, 64nffv 6895 . . . . . . . . 9 β„²β„Ž((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))
6658, 65nfmpt 5248 . . . . . . . 8 β„²β„Ž(𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))
6766nfrecs 8376 . . . . . . 7 β„²β„Žrecs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))))
6867nfcnv 5872 . . . . . 6 β„²β„Žβ—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))))
69 nfcv 2897 . . . . . 6 β„²β„Ž{𝑐}
7068, 69nfima 6061 . . . . 5 β„²β„Ž(β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐})
7170nfint 4953 . . . 4 β„²β„Žβˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑐})
72 nfcv 2897 . . . . . 6 β„²β„Ž{𝑏}
7368, 72nfima 6061 . . . . 5 β„²β„Ž(β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})
7473nfint 4953 . . . 4 β„²β„Žβˆ© (β—‘recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))β€˜((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔)))) β€œ {𝑏})
7571, 74nfel 2911 . . 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 4633 . . . . . 6 (𝑔 = 𝑐 β†’ {𝑔} = {𝑐})
7776imaeq2d 6053 . . . . 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 4948 . . . 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 4633 . . . . . 6 (β„Ž = 𝑏 β†’ {β„Ž} = {𝑏})
8079imaeq2d 6053 . . . . 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 4948 . . . 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 2817 . . . 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 595 . . 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 5213 . 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 6885 . . . . 5 (𝑔 = 𝑐 β†’ (rankβ€˜π‘”) = (rankβ€˜π‘))
86 fveq2 6885 . . . . 5 (β„Ž = 𝑏 β†’ (rankβ€˜β„Ž) = (rankβ€˜π‘))
8785, 86breqan12d 5157 . . . 4 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ↔ (rankβ€˜π‘) E (rankβ€˜π‘)))
8885, 86eqeqan12d 2740 . . . . 5 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ↔ (rankβ€˜π‘) = (rankβ€˜π‘)))
89 simpl 482 . . . . . 6 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ 𝑔 = 𝑐)
90 suceq 6424 . . . . . . . . 9 ((rankβ€˜π‘”) = (rankβ€˜π‘) β†’ suc (rankβ€˜π‘”) = suc (rankβ€˜π‘))
9185, 90syl 17 . . . . . . . 8 (𝑔 = 𝑐 β†’ suc (rankβ€˜π‘”) = suc (rankβ€˜π‘))
9291adantr 480 . . . . . . 7 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ suc (rankβ€˜π‘”) = suc (rankβ€˜π‘))
9392fveq2d 6889 . . . . . 6 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (π‘’β€˜suc (rankβ€˜π‘”)) = (π‘’β€˜suc (rankβ€˜π‘)))
94 simpr 484 . . . . . 6 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ β„Ž = 𝑏)
9589, 93, 94breq123d 5155 . . . . 5 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž ↔ 𝑐(π‘’β€˜suc (rankβ€˜π‘))𝑏))
9688, 95anbi12d 630 . . . 4 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž) ↔ ((rankβ€˜π‘) = (rankβ€˜π‘) ∧ 𝑐(π‘’β€˜suc (rankβ€˜π‘))𝑏)))
9787, 96orbi12d 915 . . 3 ((𝑔 = 𝑐 ∧ β„Ž = 𝑏) β†’ (((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž)) ↔ ((rankβ€˜π‘) E (rankβ€˜π‘) ∨ ((rankβ€˜π‘) = (rankβ€˜π‘) ∧ 𝑐(π‘’β€˜suc (rankβ€˜π‘))𝑏))))
9897cbvopabv 5214 . 2 {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))} = {βŸ¨π‘, π‘βŸ© ∣ ((rankβ€˜π‘) E (rankβ€˜π‘) ∨ ((rankβ€˜π‘) = (rankβ€˜π‘) ∧ 𝑐(π‘’β€˜suc (rankβ€˜π‘))𝑏))}
99 eqid 2726 . 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 5897 . . . . . . 7 (𝑙 = 𝑒 β†’ dom 𝑙 = dom 𝑒)
101100unieqd 4915 . . . . . . 7 (𝑙 = 𝑒 β†’ βˆͺ dom 𝑙 = βˆͺ dom 𝑒)
102100, 101eqeq12d 2742 . . . . . 6 (𝑙 = 𝑒 β†’ (dom 𝑙 = βˆͺ dom 𝑙 ↔ dom 𝑒 = βˆͺ dom 𝑒))
103 fveq1 6884 . . . . . . . . . 10 (𝑙 = 𝑒 β†’ (π‘™β€˜suc (rankβ€˜π‘”)) = (π‘’β€˜suc (rankβ€˜π‘”)))
104103breqd 5152 . . . . . . . . 9 (𝑙 = 𝑒 β†’ (𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž ↔ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))
105104anbi2d 628 . . . . . . . 8 (𝑙 = 𝑒 β†’ (((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž) ↔ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž)))
106105orbi2d 912 . . . . . . 7 (𝑙 = 𝑒 β†’ (((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž)) ↔ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))))
107106opabbidv 5207 . . . . . 6 (𝑙 = 𝑒 β†’ {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘™β€˜suc (rankβ€˜π‘”))β„Ž))} = {βŸ¨π‘”, β„ŽβŸ© ∣ ((rankβ€˜π‘”) E (rankβ€˜β„Ž) ∨ ((rankβ€˜π‘”) = (rankβ€˜β„Ž) ∧ 𝑔(π‘’β€˜suc (rankβ€˜π‘”))β„Ž))})
108 eqidd 2727 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑒 β†’ (π‘¦β€˜π‘”) = (π‘¦β€˜π‘”))
109100fveq2d 6889 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑒 β†’ (𝑅1β€˜dom 𝑙) = (𝑅1β€˜dom 𝑒))
110101fveq2d 6889 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑒 β†’ (𝑅1β€˜βˆͺ dom 𝑙) = (𝑅1β€˜βˆͺ dom 𝑒))
111 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = 𝑒 β†’ 𝑙 = 𝑒)
112111, 101fveq12d 6892 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 = 𝑒 β†’ (π‘™β€˜βˆͺ dom 𝑙) = (π‘’β€˜βˆͺ dom 𝑒))
113112breqd 5152 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑒 β†’ (𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 ↔ 𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖))
114113imbi1d 341 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑒 β†’ ((𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)) ↔ (𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))))
115110, 114raleqbidv 3336 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑒 β†’ (βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)) ↔ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))))
116115anbi2d 628 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑒 β†’ (((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))) ↔ ((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))))
117110, 116rexeqbidv 3337 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑒 β†’ (βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž))) ↔ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))))
118117opabbidv 5207 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑒 β†’ {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))} = {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})
119108, 109, 118supeq123d 9447 . . . . . . . . . . . . . . 15 (𝑙 = 𝑒 β†’ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}) = sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))}))
120119mpteq2dv 5243 . . . . . . . . . . . . . 14 (𝑙 = 𝑒 β†’ (𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑙), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑙)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑙)(𝑗(π‘™β€˜βˆͺ dom 𝑙)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})) = (𝑔 ∈ V ↦ sup((π‘¦β€˜π‘”), (𝑅1β€˜dom 𝑒), {βŸ¨π‘”, β„ŽβŸ© ∣ βˆƒπ‘– ∈ (𝑅1β€˜βˆͺ dom 𝑒)((𝑖 ∈ β„Ž ∧ Β¬ 𝑖 ∈ 𝑔) ∧ βˆ€π‘— ∈ (𝑅1β€˜βˆͺ dom 𝑒)(𝑗(π‘’β€˜βˆͺ dom 𝑒)𝑖 β†’ (𝑗 ∈ 𝑔 ↔ 𝑗 ∈ β„Ž)))})))
121109difeq1d 4116 . . . . . . . . . . . . . 14 (𝑙 = 𝑒 β†’ ((𝑅1β€˜dom 𝑙) βˆ– ran 𝑔) = ((𝑅1β€˜dom 𝑒) βˆ– ran 𝑔))
122120, 121fveq12d 6892 . . . . . . . . . . . . 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 5243 . . . . . . . . . . . 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 8375 . . . . . . . . . . . 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 5869 . . . . . . . . . 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 6052 . . . . . . . . 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 4948 . . . . . . . 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 6052 . . . . . . . . 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 4948 . . . . . . . 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 2821 . . . . . . 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 5207 . . . . . 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 4551 . . . . 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 5701 . . . . 5 (𝑙 = 𝑒 β†’ ((𝑅1β€˜dom 𝑙) Γ— (𝑅1β€˜dom 𝑙)) = ((𝑅1β€˜dom 𝑒) Γ— (𝑅1β€˜dom 𝑒)))
135133, 134ineq12d 4208 . . . 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 5254 . . 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 8375 . . 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 2997 . . . . 5 (π‘Ž = 𝑐 β†’ (π‘Ž β‰  βˆ… ↔ 𝑐 β‰  βˆ…))
142 fveq2 6885 . . . . . 6 (π‘Ž = 𝑐 β†’ (π‘¦β€˜π‘Ž) = (π‘¦β€˜π‘))
143 pweq 4611 . . . . . . . 8 (π‘Ž = 𝑐 β†’ 𝒫 π‘Ž = 𝒫 𝑐)
144143ineq1d 4206 . . . . . . 7 (π‘Ž = 𝑐 β†’ (𝒫 π‘Ž ∩ Fin) = (𝒫 𝑐 ∩ Fin))
145144difeq1d 4116 . . . . . 6 (π‘Ž = 𝑐 β†’ ((𝒫 π‘Ž ∩ Fin) βˆ– {βˆ…}) = ((𝒫 𝑐 ∩ Fin) βˆ– {βˆ…}))
146142, 145eleq12d 2821 . . . . 5 (π‘Ž = 𝑐 β†’ ((π‘¦β€˜π‘Ž) ∈ ((𝒫 π‘Ž ∩ Fin) βˆ– {βˆ…}) ↔ (π‘¦β€˜π‘) ∈ ((𝒫 𝑐 ∩ Fin) βˆ– {βˆ…})))
147141, 146imbi12d 344 . . . 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 42380 1 (πœ‘ β†’ βˆƒπ‘ 𝑏 We (𝑅1β€˜π΄))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098   β‰  wne 2934  βˆ€wral 3055  βˆƒwrex 3064  Vcvv 3468   βˆ– cdif 3940   ∩ cin 3942  βˆ…c0 4317  ifcif 4523  π’« cpw 4597  {csn 4623  βˆͺ cuni 4902  βˆ© cint 4943   class class class wbr 5141  {copab 5203   ↦ cmpt 5224   E cep 5572   We wwe 5623   Γ— cxp 5667  β—‘ccnv 5668  dom cdm 5669  ran crn 5670   β€œ cima 5672  Oncon0 6358  suc csuc 6360  β€˜cfv 6537  recscrecs 8371  Fincfn 8941  supcsup 9437  π‘…1cr1 9759  rankcrnk 9760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-2o 8468  df-map 8824  df-en 8942  df-fin 8945  df-sup 9439  df-r1 9761  df-rank 9762
This theorem is referenced by:  dfac11  42382
  Copyright terms: Public domain W3C validator