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 41374
Description: Lemma for dfac11 41375. Perform variable substitutions. This is the most we can say without invoking regularity. (Contributed by Stefan O'Rear, 20-Jan-2015.)
Hypotheses
Ref Expression
aomclem8.a (𝜑𝐴 ∈ On)
aomclem8.y (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1𝐴)(𝑎 ≠ ∅ → (𝑦𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))
Assertion
Ref Expression
aomclem8 (𝜑 → ∃𝑏 𝑏 We (𝑅1𝐴))
Distinct variable groups:   𝜑,𝑏   𝐴,𝑎,𝑏   𝑦,𝑎,𝑏
Allowed substitution hints:   𝜑(𝑦,𝑎)   𝐴(𝑦)

Proof of Theorem aomclem8
Dummy variables 𝑐 𝑑 𝑒 𝑓 𝑔 𝑖 𝑗 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elequ2 2121 . . . . . . 7 ( = 𝑏 → (𝑖𝑖𝑏))
2 elequ2 2121 . . . . . . . 8 (𝑔 = 𝑐 → (𝑖𝑔𝑖𝑐))
32notbid 317 . . . . . . 7 (𝑔 = 𝑐 → (¬ 𝑖𝑔 ↔ ¬ 𝑖𝑐))
41, 3bi2anan9r 638 . . . . . 6 ((𝑔 = 𝑐 = 𝑏) → ((𝑖 ∧ ¬ 𝑖𝑔) ↔ (𝑖𝑏 ∧ ¬ 𝑖𝑐)))
5 elequ2 2121 . . . . . . . . 9 (𝑔 = 𝑐 → (𝑗𝑔𝑗𝑐))
6 elequ2 2121 . . . . . . . . 9 ( = 𝑏 → (𝑗𝑗𝑏))
75, 6bi2bian9 639 . . . . . . . 8 ((𝑔 = 𝑐 = 𝑏) → ((𝑗𝑔𝑗) ↔ (𝑗𝑐𝑗𝑏)))
87imbi2d 340 . . . . . . 7 ((𝑔 = 𝑐 = 𝑏) → ((𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)) ↔ (𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏))))
98ralbidv 3174 . . . . . 6 ((𝑔 = 𝑐 = 𝑏) → (∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)) ↔ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏))))
104, 9anbi12d 631 . . . . 5 ((𝑔 = 𝑐 = 𝑏) → (((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗))) ↔ ((𝑖𝑏 ∧ ¬ 𝑖𝑐) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏)))))
1110rexbidv 3175 . . . 4 ((𝑔 = 𝑐 = 𝑏) → (∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗))) ↔ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖𝑏 ∧ ¬ 𝑖𝑐) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏)))))
12 elequ1 2113 . . . . . . 7 (𝑖 = 𝑑 → (𝑖𝑏𝑑𝑏))
13 elequ1 2113 . . . . . . . 8 (𝑖 = 𝑑 → (𝑖𝑐𝑑𝑐))
1413notbid 317 . . . . . . 7 (𝑖 = 𝑑 → (¬ 𝑖𝑐 ↔ ¬ 𝑑𝑐))
1512, 14anbi12d 631 . . . . . 6 (𝑖 = 𝑑 → ((𝑖𝑏 ∧ ¬ 𝑖𝑐) ↔ (𝑑𝑏 ∧ ¬ 𝑑𝑐)))
16 breq2 5109 . . . . . . . . 9 (𝑖 = 𝑑 → (𝑗(𝑒 dom 𝑒)𝑖𝑗(𝑒 dom 𝑒)𝑑))
1716imbi1d 341 . . . . . . . 8 (𝑖 = 𝑑 → ((𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏)) ↔ (𝑗(𝑒 dom 𝑒)𝑑 → (𝑗𝑐𝑗𝑏))))
1817ralbidv 3174 . . . . . . 7 (𝑖 = 𝑑 → (∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏)) ↔ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑑 → (𝑗𝑐𝑗𝑏))))
19 breq1 5108 . . . . . . . . 9 (𝑗 = 𝑓 → (𝑗(𝑒 dom 𝑒)𝑑𝑓(𝑒 dom 𝑒)𝑑))
20 elequ1 2113 . . . . . . . . . 10 (𝑗 = 𝑓 → (𝑗𝑐𝑓𝑐))
21 elequ1 2113 . . . . . . . . . 10 (𝑗 = 𝑓 → (𝑗𝑏𝑓𝑏))
2220, 21bibi12d 345 . . . . . . . . 9 (𝑗 = 𝑓 → ((𝑗𝑐𝑗𝑏) ↔ (𝑓𝑐𝑓𝑏)))
2319, 22imbi12d 344 . . . . . . . 8 (𝑗 = 𝑓 → ((𝑗(𝑒 dom 𝑒)𝑑 → (𝑗𝑐𝑗𝑏)) ↔ (𝑓(𝑒 dom 𝑒)𝑑 → (𝑓𝑐𝑓𝑏))))
2423cbvralvw 3225 . . . . . . 7 (∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑑 → (𝑗𝑐𝑗𝑏)) ↔ ∀𝑓 ∈ (𝑅1 dom 𝑒)(𝑓(𝑒 dom 𝑒)𝑑 → (𝑓𝑐𝑓𝑏)))
2518, 24bitrdi 286 . . . . . 6 (𝑖 = 𝑑 → (∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏)) ↔ ∀𝑓 ∈ (𝑅1 dom 𝑒)(𝑓(𝑒 dom 𝑒)𝑑 → (𝑓𝑐𝑓𝑏))))
2615, 25anbi12d 631 . . . . 5 (𝑖 = 𝑑 → (((𝑖𝑏 ∧ ¬ 𝑖𝑐) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏))) ↔ ((𝑑𝑏 ∧ ¬ 𝑑𝑐) ∧ ∀𝑓 ∈ (𝑅1 dom 𝑒)(𝑓(𝑒 dom 𝑒)𝑑 → (𝑓𝑐𝑓𝑏)))))
2726cbvrexvw 3226 . . . 4 (∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖𝑏 ∧ ¬ 𝑖𝑐) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏))) ↔ ∃𝑑 ∈ (𝑅1 dom 𝑒)((𝑑𝑏 ∧ ¬ 𝑑𝑐) ∧ ∀𝑓 ∈ (𝑅1 dom 𝑒)(𝑓(𝑒 dom 𝑒)𝑑 → (𝑓𝑐𝑓𝑏))))
2811, 27bitrdi 286 . . 3 ((𝑔 = 𝑐 = 𝑏) → (∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗))) ↔ ∃𝑑 ∈ (𝑅1 dom 𝑒)((𝑑𝑏 ∧ ¬ 𝑑𝑐) ∧ ∀𝑓 ∈ (𝑅1 dom 𝑒)(𝑓(𝑒 dom 𝑒)𝑑 → (𝑓𝑐𝑓𝑏)))))
2928cbvopabv 5178 . 2 {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))} = {⟨𝑐, 𝑏⟩ ∣ ∃𝑑 ∈ (𝑅1 dom 𝑒)((𝑑𝑏 ∧ ¬ 𝑑𝑐) ∧ ∀𝑓 ∈ (𝑅1 dom 𝑒)(𝑓(𝑒 dom 𝑒)𝑑 → (𝑓𝑐𝑓𝑏)))}
30 nfcv 2907 . . 3 𝑐sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))})
31 nfcv 2907 . . . 4 𝑔(𝑦𝑐)
32 nfcv 2907 . . . 4 𝑔(𝑅1‘dom 𝑒)
33 nfopab1 5175 . . . 4 𝑔{⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}
3431, 32, 33nfsup 9387 . . 3 𝑔sup((𝑦𝑐), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))})
35 fveq2 6842 . . . 4 (𝑔 = 𝑐 → (𝑦𝑔) = (𝑦𝑐))
3635supeq1d 9382 . . 3 (𝑔 = 𝑐 → sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}) = sup((𝑦𝑐), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))
3730, 34, 36cbvmpt 5216 . 2 (𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))})) = (𝑐 ∈ V ↦ sup((𝑦𝑐), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))
38 nfcv 2907 . . . 4 𝑐((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔))
39 nffvmpt1 6853 . . . 4 𝑔((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑐))
40 rneq 5891 . . . . . 6 (𝑔 = 𝑐 → ran 𝑔 = ran 𝑐)
4140difeq2d 4082 . . . . 5 (𝑔 = 𝑐 → ((𝑅1‘dom 𝑒) ∖ ran 𝑔) = ((𝑅1‘dom 𝑒) ∖ ran 𝑐))
4241fveq2d 6846 . . . 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 5216 . . 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 8320 . . 3 ((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔))) = (𝑐 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑐))) → recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) = recs((𝑐 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑐)))))
4543, 44ax-mp 5 . 2 recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) = recs((𝑐 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑐))))
46 nfv 1917 . . 3 𝑐 (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑔}) ∈ (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {})
47 nfv 1917 . . 3 𝑏 (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑔}) ∈ (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {})
48 nfmpt1 5213 . . . . . . . 8 𝑔(𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))
4948nfrecs 8321 . . . . . . 7 𝑔recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔))))
5049nfcnv 5834 . . . . . 6 𝑔recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔))))
51 nfcv 2907 . . . . . 6 𝑔{𝑐}
5250, 51nfima 6021 . . . . 5 𝑔(recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑐})
5352nfint 4917 . . . 4 𝑔 (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑐})
54 nfcv 2907 . . . . . 6 𝑔{𝑏}
5550, 54nfima 6021 . . . . 5 𝑔(recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑏})
5655nfint 4917 . . . 4 𝑔 (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑏})
5753, 56nfel 2921 . . 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 2907 . . . . . . . . 9 V
59 nfcv 2907 . . . . . . . . . . . 12 (𝑦𝑔)
60 nfcv 2907 . . . . . . . . . . . 12 (𝑅1‘dom 𝑒)
61 nfopab2 5176 . . . . . . . . . . . 12 {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}
6259, 60, 61nfsup 9387 . . . . . . . . . . 11 sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))})
6358, 62nfmpt 5212 . . . . . . . . . 10 (𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))
64 nfcv 2907 . . . . . . . . . 10 ((𝑅1‘dom 𝑒) ∖ ran 𝑔)
6563, 64nffv 6852 . . . . . . . . 9 ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔))
6658, 65nfmpt 5212 . . . . . . . 8 (𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))
6766nfrecs 8321 . . . . . . 7 recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔))))
6867nfcnv 5834 . . . . . 6 recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔))))
69 nfcv 2907 . . . . . 6 {𝑐}
7068, 69nfima 6021 . . . . 5 (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑐})
7170nfint 4917 . . . 4 (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑐})
72 nfcv 2907 . . . . . 6 {𝑏}
7368, 72nfima 6021 . . . . 5 (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑏})
7473nfint 4917 . . . 4 (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑏})
7571, 74nfel 2921 . . 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 4596 . . . . . 6 (𝑔 = 𝑐 → {𝑔} = {𝑐})
7776imaeq2d 6013 . . . . 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 4912 . . . 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 4596 . . . . . 6 ( = 𝑏 → {} = {𝑏})
8079imaeq2d 6013 . . . . 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 4912 . . . 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 2827 . . . 4 (( (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑔}) = (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑐}) ∧ (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {}) = (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑏})) → ( (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑔}) ∈ (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {}) ↔ (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑐}) ∈ (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑏})))
8378, 81, 82syl2an 596 . . 3 ((𝑔 = 𝑐 = 𝑏) → ( (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑔}) ∈ (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {}) ↔ (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑐}) ∈ (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑏})))
8446, 47, 57, 75, 83cbvopab 5177 . 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 6842 . . . . 5 (𝑔 = 𝑐 → (rank‘𝑔) = (rank‘𝑐))
86 fveq2 6842 . . . . 5 ( = 𝑏 → (rank‘) = (rank‘𝑏))
8785, 86breqan12d 5121 . . . 4 ((𝑔 = 𝑐 = 𝑏) → ((rank‘𝑔) E (rank‘) ↔ (rank‘𝑐) E (rank‘𝑏)))
8885, 86eqeqan12d 2750 . . . . 5 ((𝑔 = 𝑐 = 𝑏) → ((rank‘𝑔) = (rank‘) ↔ (rank‘𝑐) = (rank‘𝑏)))
89 simpl 483 . . . . . 6 ((𝑔 = 𝑐 = 𝑏) → 𝑔 = 𝑐)
90 suceq 6383 . . . . . . . . 9 ((rank‘𝑔) = (rank‘𝑐) → suc (rank‘𝑔) = suc (rank‘𝑐))
9185, 90syl 17 . . . . . . . 8 (𝑔 = 𝑐 → suc (rank‘𝑔) = suc (rank‘𝑐))
9291adantr 481 . . . . . . 7 ((𝑔 = 𝑐 = 𝑏) → suc (rank‘𝑔) = suc (rank‘𝑐))
9392fveq2d 6846 . . . . . 6 ((𝑔 = 𝑐 = 𝑏) → (𝑒‘suc (rank‘𝑔)) = (𝑒‘suc (rank‘𝑐)))
94 simpr 485 . . . . . 6 ((𝑔 = 𝑐 = 𝑏) → = 𝑏)
9589, 93, 94breq123d 5119 . . . . 5 ((𝑔 = 𝑐 = 𝑏) → (𝑔(𝑒‘suc (rank‘𝑔))𝑐(𝑒‘suc (rank‘𝑐))𝑏))
9688, 95anbi12d 631 . . . 4 ((𝑔 = 𝑐 = 𝑏) → (((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑒‘suc (rank‘𝑔))) ↔ ((rank‘𝑐) = (rank‘𝑏) ∧ 𝑐(𝑒‘suc (rank‘𝑐))𝑏)))
9787, 96orbi12d 917 . . 3 ((𝑔 = 𝑐 = 𝑏) → (((rank‘𝑔) E (rank‘) ∨ ((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑒‘suc (rank‘𝑔)))) ↔ ((rank‘𝑐) E (rank‘𝑏) ∨ ((rank‘𝑐) = (rank‘𝑏) ∧ 𝑐(𝑒‘suc (rank‘𝑐))𝑏))))
9897cbvopabv 5178 . 2 {⟨𝑔, ⟩ ∣ ((rank‘𝑔) E (rank‘) ∨ ((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑒‘suc (rank‘𝑔))))} = {⟨𝑐, 𝑏⟩ ∣ ((rank‘𝑐) E (rank‘𝑏) ∨ ((rank‘𝑐) = (rank‘𝑏) ∧ 𝑐(𝑒‘suc (rank‘𝑐))𝑏))}
99 eqid 2736 . 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 5859 . . . . . . 7 (𝑙 = 𝑒 → dom 𝑙 = dom 𝑒)
101100unieqd 4879 . . . . . . 7 (𝑙 = 𝑒 dom 𝑙 = dom 𝑒)
102100, 101eqeq12d 2752 . . . . . 6 (𝑙 = 𝑒 → (dom 𝑙 = dom 𝑙 ↔ dom 𝑒 = dom 𝑒))
103 fveq1 6841 . . . . . . . . . 10 (𝑙 = 𝑒 → (𝑙‘suc (rank‘𝑔)) = (𝑒‘suc (rank‘𝑔)))
104103breqd 5116 . . . . . . . . 9 (𝑙 = 𝑒 → (𝑔(𝑙‘suc (rank‘𝑔))𝑔(𝑒‘suc (rank‘𝑔))))
105104anbi2d 629 . . . . . . . 8 (𝑙 = 𝑒 → (((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑙‘suc (rank‘𝑔))) ↔ ((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑒‘suc (rank‘𝑔)))))
106105orbi2d 914 . . . . . . 7 (𝑙 = 𝑒 → (((rank‘𝑔) E (rank‘) ∨ ((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑙‘suc (rank‘𝑔)))) ↔ ((rank‘𝑔) E (rank‘) ∨ ((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑒‘suc (rank‘𝑔))))))
107106opabbidv 5171 . . . . . 6 (𝑙 = 𝑒 → {⟨𝑔, ⟩ ∣ ((rank‘𝑔) E (rank‘) ∨ ((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑙‘suc (rank‘𝑔))))} = {⟨𝑔, ⟩ ∣ ((rank‘𝑔) E (rank‘) ∨ ((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑒‘suc (rank‘𝑔))))})
108 eqidd 2737 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑒 → (𝑦𝑔) = (𝑦𝑔))
109100fveq2d 6846 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑒 → (𝑅1‘dom 𝑙) = (𝑅1‘dom 𝑒))
110101fveq2d 6846 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑒 → (𝑅1 dom 𝑙) = (𝑅1 dom 𝑒))
111 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = 𝑒𝑙 = 𝑒)
112111, 101fveq12d 6849 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 = 𝑒 → (𝑙 dom 𝑙) = (𝑒 dom 𝑒))
113112breqd 5116 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑒 → (𝑗(𝑙 dom 𝑙)𝑖𝑗(𝑒 dom 𝑒)𝑖))
114113imbi1d 341 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑒 → ((𝑗(𝑙 dom 𝑙)𝑖 → (𝑗𝑔𝑗)) ↔ (𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗))))
115110, 114raleqbidv 3319 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑒 → (∀𝑗 ∈ (𝑅1 dom 𝑙)(𝑗(𝑙 dom 𝑙)𝑖 → (𝑗𝑔𝑗)) ↔ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗))))
116115anbi2d 629 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑒 → (((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑙)(𝑗(𝑙 dom 𝑙)𝑖 → (𝑗𝑔𝑗))) ↔ ((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))))
117110, 116rexeqbidv 3320 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑒 → (∃𝑖 ∈ (𝑅1 dom 𝑙)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑙)(𝑗(𝑙 dom 𝑙)𝑖 → (𝑗𝑔𝑗))) ↔ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))))
118117opabbidv 5171 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑒 → {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑙)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑙)(𝑗(𝑙 dom 𝑙)𝑖 → (𝑗𝑔𝑗)))} = {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))})
119108, 109, 118supeq123d 9386 . . . . . . . . . . . . . . 15 (𝑙 = 𝑒 → sup((𝑦𝑔), (𝑅1‘dom 𝑙), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑙)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑙)(𝑗(𝑙 dom 𝑙)𝑖 → (𝑗𝑔𝑗)))}) = sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))
120119mpteq2dv 5207 . . . . . . . . . . . . . 14 (𝑙 = 𝑒 → (𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑙), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑙)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑙)(𝑗(𝑙 dom 𝑙)𝑖 → (𝑗𝑔𝑗)))})) = (𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))})))
121109difeq1d 4081 . . . . . . . . . . . . . 14 (𝑙 = 𝑒 → ((𝑅1‘dom 𝑙) ∖ ran 𝑔) = ((𝑅1‘dom 𝑒) ∖ ran 𝑔))
122120, 121fveq12d 6849 . . . . . . . . . . . . 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 5207 . . . . . . . . . . . 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 8320 . . . . . . . . . . . 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 5831 . . . . . . . . . 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 6012 . . . . . . . . 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 4912 . . . . . . . 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 6012 . . . . . . . . 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 4912 . . . . . . . 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 5171 . . . . . 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 4514 . . . . 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 5665 . . . . 5 (𝑙 = 𝑒 → ((𝑅1‘dom 𝑙) × (𝑅1‘dom 𝑙)) = ((𝑅1‘dom 𝑒) × (𝑅1‘dom 𝑒)))
135133, 134ineq12d 4173 . . . 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 5218 . . 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 8320 . . 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 3006 . . . . 5 (𝑎 = 𝑐 → (𝑎 ≠ ∅ ↔ 𝑐 ≠ ∅))
142 fveq2 6842 . . . . . 6 (𝑎 = 𝑐 → (𝑦𝑎) = (𝑦𝑐))
143 pweq 4574 . . . . . . . 8 (𝑎 = 𝑐 → 𝒫 𝑎 = 𝒫 𝑐)
144143ineq1d 4171 . . . . . . 7 (𝑎 = 𝑐 → (𝒫 𝑎 ∩ Fin) = (𝒫 𝑐 ∩ Fin))
145144difeq1d 4081 . . . . . 6 (𝑎 = 𝑐 → ((𝒫 𝑎 ∩ Fin) ∖ {∅}) = ((𝒫 𝑐 ∩ Fin) ∖ {∅}))
146142, 145eleq12d 2832 . . . . 5 (𝑎 = 𝑐 → ((𝑦𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅}) ↔ (𝑦𝑐) ∈ ((𝒫 𝑐 ∩ Fin) ∖ {∅})))
147141, 146imbi12d 344 . . . 4 (𝑎 = 𝑐 → ((𝑎 ≠ ∅ → (𝑦𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})) ↔ (𝑐 ≠ ∅ → (𝑦𝑐) ∈ ((𝒫 𝑐 ∩ Fin) ∖ {∅}))))
148147cbvralvw 3225 . . 3 (∀𝑎 ∈ 𝒫 (𝑅1𝐴)(𝑎 ≠ ∅ → (𝑦𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})) ↔ ∀𝑐 ∈ 𝒫 (𝑅1𝐴)(𝑐 ≠ ∅ → (𝑦𝑐) ∈ ((𝒫 𝑐 ∩ Fin) ∖ {∅})))
149140, 148sylib 217 . 2 (𝜑 → ∀𝑐 ∈ 𝒫 (𝑅1𝐴)(𝑐 ≠ ∅ → (𝑦𝑐) ∈ ((𝒫 𝑐 ∩ Fin) ∖ {∅})))
15029, 37, 45, 84, 98, 99, 138, 139, 149aomclem7 41373 1 (𝜑 → ∃𝑏 𝑏 We (𝑅1𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wex 1781  wcel 2106  wne 2943  wral 3064  wrex 3073  Vcvv 3445  cdif 3907  cin 3909  c0 4282  ifcif 4486  𝒫 cpw 4560  {csn 4586   cuni 4865   cint 4907   class class class wbr 5105  {copab 5167  cmpt 5188   E cep 5536   We wwe 5587   × cxp 5631  ccnv 5632  dom cdm 5633  ran crn 5634  cima 5636  Oncon0 6317  suc csuc 6319  cfv 6496  recscrecs 8316  Fincfn 8883  supcsup 9376  𝑅1cr1 9698  rankcrnk 9699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-map 8767  df-en 8884  df-fin 8887  df-sup 9378  df-r1 9700  df-rank 9701
This theorem is referenced by:  dfac11  41375
  Copyright terms: Public domain W3C validator