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 36649
 Description: Lemma for dfac11 36650. 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 1991 . . . . . . 7 ( = 𝑏 → (𝑖𝑖𝑏))
2 elequ2 1991 . . . . . . . 8 (𝑔 = 𝑐 → (𝑖𝑔𝑖𝑐))
32notbid 307 . . . . . . 7 (𝑔 = 𝑐 → (¬ 𝑖𝑔 ↔ ¬ 𝑖𝑐))
41, 3bi2anan9r 914 . . . . . 6 ((𝑔 = 𝑐 = 𝑏) → ((𝑖 ∧ ¬ 𝑖𝑔) ↔ (𝑖𝑏 ∧ ¬ 𝑖𝑐)))
5 elequ2 1991 . . . . . . . . 9 (𝑔 = 𝑐 → (𝑗𝑔𝑗𝑐))
6 elequ2 1991 . . . . . . . . 9 ( = 𝑏 → (𝑗𝑗𝑏))
75, 6bi2bian9 915 . . . . . . . 8 ((𝑔 = 𝑐 = 𝑏) → ((𝑗𝑔𝑗) ↔ (𝑗𝑐𝑗𝑏)))
87imbi2d 329 . . . . . . 7 ((𝑔 = 𝑐 = 𝑏) → ((𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)) ↔ (𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏))))
98ralbidv 2969 . . . . . 6 ((𝑔 = 𝑐 = 𝑏) → (∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)) ↔ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏))))
104, 9anbi12d 743 . . . . 5 ((𝑔 = 𝑐 = 𝑏) → (((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗))) ↔ ((𝑖𝑏 ∧ ¬ 𝑖𝑐) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏)))))
1110rexbidv 3034 . . . 4 ((𝑔 = 𝑐 = 𝑏) → (∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗))) ↔ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖𝑏 ∧ ¬ 𝑖𝑐) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏)))))
12 elequ1 1984 . . . . . . 7 (𝑖 = 𝑑 → (𝑖𝑏𝑑𝑏))
13 elequ1 1984 . . . . . . . 8 (𝑖 = 𝑑 → (𝑖𝑐𝑑𝑐))
1413notbid 307 . . . . . . 7 (𝑖 = 𝑑 → (¬ 𝑖𝑐 ↔ ¬ 𝑑𝑐))
1512, 14anbi12d 743 . . . . . 6 (𝑖 = 𝑑 → ((𝑖𝑏 ∧ ¬ 𝑖𝑐) ↔ (𝑑𝑏 ∧ ¬ 𝑑𝑐)))
16 breq2 4587 . . . . . . . . 9 (𝑖 = 𝑑 → (𝑗(𝑒 dom 𝑒)𝑖𝑗(𝑒 dom 𝑒)𝑑))
1716imbi1d 330 . . . . . . . 8 (𝑖 = 𝑑 → ((𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏)) ↔ (𝑗(𝑒 dom 𝑒)𝑑 → (𝑗𝑐𝑗𝑏))))
1817ralbidv 2969 . . . . . . 7 (𝑖 = 𝑑 → (∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏)) ↔ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑑 → (𝑗𝑐𝑗𝑏))))
19 breq1 4586 . . . . . . . . 9 (𝑗 = 𝑓 → (𝑗(𝑒 dom 𝑒)𝑑𝑓(𝑒 dom 𝑒)𝑑))
20 elequ1 1984 . . . . . . . . . 10 (𝑗 = 𝑓 → (𝑗𝑐𝑓𝑐))
21 elequ1 1984 . . . . . . . . . 10 (𝑗 = 𝑓 → (𝑗𝑏𝑓𝑏))
2220, 21bibi12d 334 . . . . . . . . 9 (𝑗 = 𝑓 → ((𝑗𝑐𝑗𝑏) ↔ (𝑓𝑐𝑓𝑏)))
2319, 22imbi12d 333 . . . . . . . 8 (𝑗 = 𝑓 → ((𝑗(𝑒 dom 𝑒)𝑑 → (𝑗𝑐𝑗𝑏)) ↔ (𝑓(𝑒 dom 𝑒)𝑑 → (𝑓𝑐𝑓𝑏))))
2423cbvralv 3147 . . . . . . 7 (∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑑 → (𝑗𝑐𝑗𝑏)) ↔ ∀𝑓 ∈ (𝑅1 dom 𝑒)(𝑓(𝑒 dom 𝑒)𝑑 → (𝑓𝑐𝑓𝑏)))
2518, 24syl6bb 275 . . . . . 6 (𝑖 = 𝑑 → (∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏)) ↔ ∀𝑓 ∈ (𝑅1 dom 𝑒)(𝑓(𝑒 dom 𝑒)𝑑 → (𝑓𝑐𝑓𝑏))))
2615, 25anbi12d 743 . . . . 5 (𝑖 = 𝑑 → (((𝑖𝑏 ∧ ¬ 𝑖𝑐) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏))) ↔ ((𝑑𝑏 ∧ ¬ 𝑑𝑐) ∧ ∀𝑓 ∈ (𝑅1 dom 𝑒)(𝑓(𝑒 dom 𝑒)𝑑 → (𝑓𝑐𝑓𝑏)))))
2726cbvrexv 3148 . . . 4 (∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖𝑏 ∧ ¬ 𝑖𝑐) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑐𝑗𝑏))) ↔ ∃𝑑 ∈ (𝑅1 dom 𝑒)((𝑑𝑏 ∧ ¬ 𝑑𝑐) ∧ ∀𝑓 ∈ (𝑅1 dom 𝑒)(𝑓(𝑒 dom 𝑒)𝑑 → (𝑓𝑐𝑓𝑏))))
2811, 27syl6bb 275 . . 3 ((𝑔 = 𝑐 = 𝑏) → (∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗))) ↔ ∃𝑑 ∈ (𝑅1 dom 𝑒)((𝑑𝑏 ∧ ¬ 𝑑𝑐) ∧ ∀𝑓 ∈ (𝑅1 dom 𝑒)(𝑓(𝑒 dom 𝑒)𝑑 → (𝑓𝑐𝑓𝑏)))))
2928cbvopabv 4654 . 2 {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))} = {⟨𝑐, 𝑏⟩ ∣ ∃𝑑 ∈ (𝑅1 dom 𝑒)((𝑑𝑏 ∧ ¬ 𝑑𝑐) ∧ ∀𝑓 ∈ (𝑅1 dom 𝑒)(𝑓(𝑒 dom 𝑒)𝑑 → (𝑓𝑐𝑓𝑏)))}
30 nfcv 2751 . . 3 𝑐sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))})
31 nfcv 2751 . . . 4 𝑔(𝑦𝑐)
32 nfcv 2751 . . . 4 𝑔(𝑅1‘dom 𝑒)
33 nfopab1 4651 . . . 4 𝑔{⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}
3431, 32, 33nfsup 8240 . . 3 𝑔sup((𝑦𝑐), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))})
35 fveq2 6103 . . . 4 (𝑔 = 𝑐 → (𝑦𝑔) = (𝑦𝑐))
3635supeq1d 8235 . . 3 (𝑔 = 𝑐 → sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}) = sup((𝑦𝑐), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))
3730, 34, 36cbvmpt 4677 . 2 (𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))})) = (𝑐 ∈ V ↦ sup((𝑦𝑐), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))
38 nfcv 2751 . . . 4 𝑐((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔))
39 nffvmpt1 6111 . . . 4 𝑔((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑐))
40 rneq 5272 . . . . . 6 (𝑔 = 𝑐 → ran 𝑔 = ran 𝑐)
4140difeq2d 3690 . . . . 5 (𝑔 = 𝑐 → ((𝑅1‘dom 𝑒) ∖ ran 𝑔) = ((𝑅1‘dom 𝑒) ∖ ran 𝑐))
4241fveq2d 6107 . . . 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 4677 . . 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 7357 . . 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 1830 . . 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 1830 . . 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 4675 . . . . . . . 8 𝑔(𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))
4948nfrecs 7358 . . . . . . 7 𝑔recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔))))
5049nfcnv 5223 . . . . . 6 𝑔recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔))))
51 nfcv 2751 . . . . . 6 𝑔{𝑐}
5250, 51nfima 5393 . . . . 5 𝑔(recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑐})
5352nfint 4421 . . . 4 𝑔 (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑐})
54 nfcv 2751 . . . . . 6 𝑔{𝑏}
5550, 54nfima 5393 . . . . 5 𝑔(recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑏})
5655nfint 4421 . . . 4 𝑔 (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑏})
5753, 56nfel 2763 . . 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 2751 . . . . . . . . 9 V
59 nfcv 2751 . . . . . . . . . . . 12 (𝑦𝑔)
60 nfcv 2751 . . . . . . . . . . . 12 (𝑅1‘dom 𝑒)
61 nfopab2 4652 . . . . . . . . . . . 12 {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}
6259, 60, 61nfsup 8240 . . . . . . . . . . 11 sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))})
6358, 62nfmpt 4674 . . . . . . . . . 10 (𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))
64 nfcv 2751 . . . . . . . . . 10 ((𝑅1‘dom 𝑒) ∖ ran 𝑔)
6563, 64nffv 6110 . . . . . . . . 9 ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔))
6658, 65nfmpt 4674 . . . . . . . 8 (𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))
6766nfrecs 7358 . . . . . . 7 recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔))))
6867nfcnv 5223 . . . . . 6 recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔))))
69 nfcv 2751 . . . . . 6 {𝑐}
7068, 69nfima 5393 . . . . 5 (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑐})
7170nfint 4421 . . . 4 (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑐})
72 nfcv 2751 . . . . . 6 {𝑏}
7368, 72nfima 5393 . . . . 5 (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑏})
7473nfint 4421 . . . 4 (recs((𝑔 ∈ V ↦ ((𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))‘((𝑅1‘dom 𝑒) ∖ ran 𝑔)))) “ {𝑏})
7571, 74nfel 2763 . . 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 4135 . . . . . 6 (𝑔 = 𝑐 → {𝑔} = {𝑐})
7776imaeq2d 5385 . . . . 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 4415 . . . 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 4135 . . . . . 6 ( = 𝑏 → {} = {𝑏})
8079imaeq2d 5385 . . . . 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 4415 . . . 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 2678 . . . 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 493 . . 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 4653 . 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 6103 . . . . 5 (𝑔 = 𝑐 → (rank‘𝑔) = (rank‘𝑐))
86 fveq2 6103 . . . . 5 ( = 𝑏 → (rank‘) = (rank‘𝑏))
8785, 86breqan12d 4599 . . . 4 ((𝑔 = 𝑐 = 𝑏) → ((rank‘𝑔) E (rank‘) ↔ (rank‘𝑐) E (rank‘𝑏)))
8885, 86eqeqan12d 2626 . . . . 5 ((𝑔 = 𝑐 = 𝑏) → ((rank‘𝑔) = (rank‘) ↔ (rank‘𝑐) = (rank‘𝑏)))
89 simpl 472 . . . . . 6 ((𝑔 = 𝑐 = 𝑏) → 𝑔 = 𝑐)
90 suceq 5707 . . . . . . . . 9 ((rank‘𝑔) = (rank‘𝑐) → suc (rank‘𝑔) = suc (rank‘𝑐))
9185, 90syl 17 . . . . . . . 8 (𝑔 = 𝑐 → suc (rank‘𝑔) = suc (rank‘𝑐))
9291adantr 480 . . . . . . 7 ((𝑔 = 𝑐 = 𝑏) → suc (rank‘𝑔) = suc (rank‘𝑐))
9392fveq2d 6107 . . . . . 6 ((𝑔 = 𝑐 = 𝑏) → (𝑒‘suc (rank‘𝑔)) = (𝑒‘suc (rank‘𝑐)))
94 simpr 476 . . . . . 6 ((𝑔 = 𝑐 = 𝑏) → = 𝑏)
9589, 93, 94breq123d 4597 . . . . 5 ((𝑔 = 𝑐 = 𝑏) → (𝑔(𝑒‘suc (rank‘𝑔))𝑐(𝑒‘suc (rank‘𝑐))𝑏))
9688, 95anbi12d 743 . . . 4 ((𝑔 = 𝑐 = 𝑏) → (((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑒‘suc (rank‘𝑔))) ↔ ((rank‘𝑐) = (rank‘𝑏) ∧ 𝑐(𝑒‘suc (rank‘𝑐))𝑏)))
9787, 96orbi12d 742 . . 3 ((𝑔 = 𝑐 = 𝑏) → (((rank‘𝑔) E (rank‘) ∨ ((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑒‘suc (rank‘𝑔)))) ↔ ((rank‘𝑐) E (rank‘𝑏) ∨ ((rank‘𝑐) = (rank‘𝑏) ∧ 𝑐(𝑒‘suc (rank‘𝑐))𝑏))))
9897cbvopabv 4654 . 2 {⟨𝑔, ⟩ ∣ ((rank‘𝑔) E (rank‘) ∨ ((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑒‘suc (rank‘𝑔))))} = {⟨𝑐, 𝑏⟩ ∣ ((rank‘𝑐) E (rank‘𝑏) ∨ ((rank‘𝑐) = (rank‘𝑏) ∧ 𝑐(𝑒‘suc (rank‘𝑐))𝑏))}
99 eqid 2610 . 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 5246 . . . . . . 7 (𝑙 = 𝑒 → dom 𝑙 = dom 𝑒)
101100unieqd 4382 . . . . . . 7 (𝑙 = 𝑒 dom 𝑙 = dom 𝑒)
102100, 101eqeq12d 2625 . . . . . 6 (𝑙 = 𝑒 → (dom 𝑙 = dom 𝑙 ↔ dom 𝑒 = dom 𝑒))
103 fveq1 6102 . . . . . . . . . 10 (𝑙 = 𝑒 → (𝑙‘suc (rank‘𝑔)) = (𝑒‘suc (rank‘𝑔)))
104103breqd 4594 . . . . . . . . 9 (𝑙 = 𝑒 → (𝑔(𝑙‘suc (rank‘𝑔))𝑔(𝑒‘suc (rank‘𝑔))))
105104anbi2d 736 . . . . . . . 8 (𝑙 = 𝑒 → (((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑙‘suc (rank‘𝑔))) ↔ ((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑒‘suc (rank‘𝑔)))))
106105orbi2d 734 . . . . . . 7 (𝑙 = 𝑒 → (((rank‘𝑔) E (rank‘) ∨ ((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑙‘suc (rank‘𝑔)))) ↔ ((rank‘𝑔) E (rank‘) ∨ ((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑒‘suc (rank‘𝑔))))))
107106opabbidv 4648 . . . . . 6 (𝑙 = 𝑒 → {⟨𝑔, ⟩ ∣ ((rank‘𝑔) E (rank‘) ∨ ((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑙‘suc (rank‘𝑔))))} = {⟨𝑔, ⟩ ∣ ((rank‘𝑔) E (rank‘) ∨ ((rank‘𝑔) = (rank‘) ∧ 𝑔(𝑒‘suc (rank‘𝑔))))})
108 eqidd 2611 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑒 → (𝑦𝑔) = (𝑦𝑔))
109100fveq2d 6107 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑒 → (𝑅1‘dom 𝑙) = (𝑅1‘dom 𝑒))
110101fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑒 → (𝑅1 dom 𝑙) = (𝑅1 dom 𝑒))
111 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑙 = 𝑒𝑙 = 𝑒)
112111, 101fveq12d 6109 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 = 𝑒 → (𝑙 dom 𝑙) = (𝑒 dom 𝑒))
113112breqd 4594 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑒 → (𝑗(𝑙 dom 𝑙)𝑖𝑗(𝑒 dom 𝑒)𝑖))
114113imbi1d 330 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑒 → ((𝑗(𝑙 dom 𝑙)𝑖 → (𝑗𝑔𝑗)) ↔ (𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗))))
115110, 114raleqbidv 3129 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑒 → (∀𝑗 ∈ (𝑅1 dom 𝑙)(𝑗(𝑙 dom 𝑙)𝑖 → (𝑗𝑔𝑗)) ↔ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗))))
116115anbi2d 736 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑒 → (((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑙)(𝑗(𝑙 dom 𝑙)𝑖 → (𝑗𝑔𝑗))) ↔ ((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))))
117110, 116rexeqbidv 3130 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑒 → (∃𝑖 ∈ (𝑅1 dom 𝑙)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑙)(𝑗(𝑙 dom 𝑙)𝑖 → (𝑗𝑔𝑗))) ↔ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))))
118117opabbidv 4648 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑒 → {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑙)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑙)(𝑗(𝑙 dom 𝑙)𝑖 → (𝑗𝑔𝑗)))} = {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))})
119108, 109, 118supeq123d 8239 . . . . . . . . . . . . . . 15 (𝑙 = 𝑒 → sup((𝑦𝑔), (𝑅1‘dom 𝑙), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑙)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑙)(𝑗(𝑙 dom 𝑙)𝑖 → (𝑗𝑔𝑗)))}) = sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))}))
120119mpteq2dv 4673 . . . . . . . . . . . . . 14 (𝑙 = 𝑒 → (𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑙), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑙)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑙)(𝑗(𝑙 dom 𝑙)𝑖 → (𝑗𝑔𝑗)))})) = (𝑔 ∈ V ↦ sup((𝑦𝑔), (𝑅1‘dom 𝑒), {⟨𝑔, ⟩ ∣ ∃𝑖 ∈ (𝑅1 dom 𝑒)((𝑖 ∧ ¬ 𝑖𝑔) ∧ ∀𝑗 ∈ (𝑅1 dom 𝑒)(𝑗(𝑒 dom 𝑒)𝑖 → (𝑗𝑔𝑗)))})))
121109difeq1d 3689 . . . . . . . . . . . . . 14 (𝑙 = 𝑒 → ((𝑅1‘dom 𝑙) ∖ ran 𝑔) = ((𝑅1‘dom 𝑒) ∖ ran 𝑔))
122120, 121fveq12d 6109 . . . . . . . . . . . . 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 4673 . . . . . . . . . . . 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 7357 . . . . . . . . . . . 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 5220 . . . . . . . . . 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 5384 . . . . . . . . 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 4415 . . . . . . . 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 5384 . . . . . . . . 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 4415 . . . . . . . 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 2682 . . . . . . 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 4648 . . . . . 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 4063 . . . . 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 5065 . . . . 5 (𝑙 = 𝑒 → ((𝑅1‘dom 𝑙) × (𝑅1‘dom 𝑙)) = ((𝑅1‘dom 𝑒) × (𝑅1‘dom 𝑒)))
135133, 134ineq12d 3777 . . . 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 4678 . . 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 7357 . . 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 2844 . . . . 5 (𝑎 = 𝑐 → (𝑎 ≠ ∅ ↔ 𝑐 ≠ ∅))
142 fveq2 6103 . . . . . 6 (𝑎 = 𝑐 → (𝑦𝑎) = (𝑦𝑐))
143 pweq 4111 . . . . . . . 8 (𝑎 = 𝑐 → 𝒫 𝑎 = 𝒫 𝑐)
144143ineq1d 3775 . . . . . . 7 (𝑎 = 𝑐 → (𝒫 𝑎 ∩ Fin) = (𝒫 𝑐 ∩ Fin))
145144difeq1d 3689 . . . . . 6 (𝑎 = 𝑐 → ((𝒫 𝑎 ∩ Fin) ∖ {∅}) = ((𝒫 𝑐 ∩ Fin) ∖ {∅}))
146142, 145eleq12d 2682 . . . . 5 (𝑎 = 𝑐 → ((𝑦𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅}) ↔ (𝑦𝑐) ∈ ((𝒫 𝑐 ∩ Fin) ∖ {∅})))
147141, 146imbi12d 333 . . . 4 (𝑎 = 𝑐 → ((𝑎 ≠ ∅ → (𝑦𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})) ↔ (𝑐 ≠ ∅ → (𝑦𝑐) ∈ ((𝒫 𝑐 ∩ Fin) ∖ {∅}))))
148147cbvralv 3147 . . 3 (∀𝑎 ∈ 𝒫 (𝑅1𝐴)(𝑎 ≠ ∅ → (𝑦𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})) ↔ ∀𝑐 ∈ 𝒫 (𝑅1𝐴)(𝑐 ≠ ∅ → (𝑦𝑐) ∈ ((𝒫 𝑐 ∩ Fin) ∖ {∅})))
149140, 148sylib 207 . 2 (𝜑 → ∀𝑐 ∈ 𝒫 (𝑅1𝐴)(𝑐 ≠ ∅ → (𝑦𝑐) ∈ ((𝒫 𝑐 ∩ Fin) ∖ {∅})))
15029, 37, 45, 84, 98, 99, 138, 139, 149aomclem7 36648 1 (𝜑 → ∃𝑏 𝑏 We (𝑅1𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∩ cin 3539  ∅c0 3874  ifcif 4036  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372  ∩ cint 4410   class class class wbr 4583  {copab 4642   ↦ cmpt 4643   E cep 4947   We wwe 4996   × cxp 5036  ◡ccnv 5037  dom cdm 5038  ran crn 5039   “ cima 5041  Oncon0 5640  suc csuc 5642  ‘cfv 5804  recscrecs 7354  Fincfn 7841  supcsup 8229  𝑅1cr1 8508  rankcrnk 8509 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-er 7629  df-map 7746  df-en 7842  df-fin 7845  df-sup 8231  df-r1 8510  df-rank 8511 This theorem is referenced by:  dfac11  36650
 Copyright terms: Public domain W3C validator