Metamath Proof Explorer

Theorem aomclem8

Description: Lemma for dfac11 . Perform variable substitutions. This is the most we can say without invoking regularity. (Contributed by Stefan O'Rear, 20-Jan-2015)

Ref Expression
Hypotheses aomclem8.a ⊢ ( 𝜑 → 𝐴 ∈ On )
aomclem8.y ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
Assertion aomclem8 ( 𝜑 → ∃ 𝑏 𝑏 We ( 𝑅1 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 aomclem8.a ⊢ ( 𝜑 → 𝐴 ∈ On )
2 aomclem8.y ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) )
3 elequ2 ⊢ ( ℎ = 𝑏 → ( 𝑖 ∈ ℎ ↔ 𝑖 ∈ 𝑏 ) )
4 elequ2 ⊢ ( 𝑔 = 𝑐 → ( 𝑖 ∈ 𝑔 ↔ 𝑖 ∈ 𝑐 ) )
5 4 notbid ⊢ ( 𝑔 = 𝑐 → ( ¬ 𝑖 ∈ 𝑔 ↔ ¬ 𝑖 ∈ 𝑐 ) )
6 3 5 bi2anan9r ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ↔ ( 𝑖 ∈ 𝑏 ∧ ¬ 𝑖 ∈ 𝑐 ) ) )
7 elequ2 ⊢ ( 𝑔 = 𝑐 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ 𝑐 ) )
8 elequ2 ⊢ ( ℎ = 𝑏 → ( 𝑗 ∈ ℎ ↔ 𝑗 ∈ 𝑏 ) )
9 7 8 bi2bian9 ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → ( ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ↔ ( 𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏 ) ) )
10 9 imbi2d ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → ( ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ↔ ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏 ) ) ) )
11 10 ralbidv ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → ( ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ↔ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏 ) ) ) )
12 6 11 anbi12d ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → ( ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) ↔ ( ( 𝑖 ∈ 𝑏 ∧ ¬ 𝑖 ∈ 𝑐 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏 ) ) ) ) )
13 12 rexbidv ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → ( ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) ↔ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ 𝑏 ∧ ¬ 𝑖 ∈ 𝑐 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏 ) ) ) ) )
14 elequ1 ⊢ ( 𝑖 = 𝑑 → ( 𝑖 ∈ 𝑏 ↔ 𝑑 ∈ 𝑏 ) )
15 elequ1 ⊢ ( 𝑖 = 𝑑 → ( 𝑖 ∈ 𝑐 ↔ 𝑑 ∈ 𝑐 ) )
16 15 notbid ⊢ ( 𝑖 = 𝑑 → ( ¬ 𝑖 ∈ 𝑐 ↔ ¬ 𝑑 ∈ 𝑐 ) )
17 14 16 anbi12d ⊢ ( 𝑖 = 𝑑 → ( ( 𝑖 ∈ 𝑏 ∧ ¬ 𝑖 ∈ 𝑐 ) ↔ ( 𝑑 ∈ 𝑏 ∧ ¬ 𝑑 ∈ 𝑐 ) ) )
18 breq2 ⊢ ( 𝑖 = 𝑑 → ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 ↔ 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑑 ) )
19 18 imbi1d ⊢ ( 𝑖 = 𝑑 → ( ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏 ) ) ↔ ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑑 → ( 𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏 ) ) ) )
20 19 ralbidv ⊢ ( 𝑖 = 𝑑 → ( ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏 ) ) ↔ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑑 → ( 𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏 ) ) ) )
21 breq1 ⊢ ( 𝑗 = 𝑓 → ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑑 ↔ 𝑓 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑑 ) )
22 elequ1 ⊢ ( 𝑗 = 𝑓 → ( 𝑗 ∈ 𝑐 ↔ 𝑓 ∈ 𝑐 ) )
23 elequ1 ⊢ ( 𝑗 = 𝑓 → ( 𝑗 ∈ 𝑏 ↔ 𝑓 ∈ 𝑏 ) )
24 22 23 bibi12d ⊢ ( 𝑗 = 𝑓 → ( ( 𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏 ) ↔ ( 𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏 ) ) )
25 21 24 imbi12d ⊢ ( 𝑗 = 𝑓 → ( ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑑 → ( 𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏 ) ) ↔ ( 𝑓 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑑 → ( 𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏 ) ) ) )
26 25 cbvralvw ⊢ ( ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑑 → ( 𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏 ) ) ↔ ∀ 𝑓 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑓 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑑 → ( 𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏 ) ) )
27 20 26 bitrdi ⊢ ( 𝑖 = 𝑑 → ( ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏 ) ) ↔ ∀ 𝑓 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑓 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑑 → ( 𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏 ) ) ) )
28 17 27 anbi12d ⊢ ( 𝑖 = 𝑑 → ( ( ( 𝑖 ∈ 𝑏 ∧ ¬ 𝑖 ∈ 𝑐 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏 ) ) ) ↔ ( ( 𝑑 ∈ 𝑏 ∧ ¬ 𝑑 ∈ 𝑐 ) ∧ ∀ 𝑓 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑓 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑑 → ( 𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏 ) ) ) ) )
29 28 cbvrexvw ⊢ ( ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ 𝑏 ∧ ¬ 𝑖 ∈ 𝑐 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑐 ↔ 𝑗 ∈ 𝑏 ) ) ) ↔ ∃ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑑 ∈ 𝑏 ∧ ¬ 𝑑 ∈ 𝑐 ) ∧ ∀ 𝑓 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑓 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑑 → ( 𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏 ) ) ) )
30 13 29 bitrdi ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → ( ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) ↔ ∃ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑑 ∈ 𝑏 ∧ ¬ 𝑑 ∈ 𝑐 ) ∧ ∀ 𝑓 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑓 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑑 → ( 𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏 ) ) ) ) )
31 30 cbvopabv ⊢ { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } = { ⟨ 𝑐 , 𝑏 ⟩ ∣ ∃ 𝑑 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑑 ∈ 𝑏 ∧ ¬ 𝑑 ∈ 𝑐 ) ∧ ∀ 𝑓 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑓 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑑 → ( 𝑓 ∈ 𝑐 ↔ 𝑓 ∈ 𝑏 ) ) ) }
32 nfcv ⊢ Ⅎ 𝑐 sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } )
33 nfcv ⊢ Ⅎ 𝑔 ( 𝑦 ‘ 𝑐 )
34 nfcv ⊢ Ⅎ 𝑔 ( 𝑅1 ‘ dom 𝑒 )
35 nfopab1 ⊢ Ⅎ 𝑔 { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) }
36 33 34 35 nfsup ⊢ Ⅎ 𝑔 sup ( ( 𝑦 ‘ 𝑐 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } )
37 fveq2 ⊢ ( 𝑔 = 𝑐 → ( 𝑦 ‘ 𝑔 ) = ( 𝑦 ‘ 𝑐 ) )
38 37 supeq1d ⊢ ( 𝑔 = 𝑐 → sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) = sup ( ( 𝑦 ‘ 𝑐 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) )
39 32 36 38 cbvmpt ⊢ ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) = ( 𝑐 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑐 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) )
40 nfcv ⊢ Ⅎ 𝑐 ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) )
41 nffvmpt1 ⊢ Ⅎ 𝑔 ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑐 ) )
42 rneq ⊢ ( 𝑔 = 𝑐 → ran 𝑔 = ran 𝑐 )
43 42 difeq2d ⊢ ( 𝑔 = 𝑐 → ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) = ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑐 ) )
44 43 fveq2d ⊢ ( 𝑔 = 𝑐 → ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) = ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑐 ) ) )
45 40 41 44 cbvmpt ⊢ ( 𝑔 ∈ 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 𝑐 ) ) )
46 recseq ⊢ ( ( 𝑔 ∈ 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 𝑐 ) ) ) ) )
47 45 46 ax-mp ⊢ 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 nfv ⊢ Ⅎ 𝑐 ∩ ( ◡ 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 𝑔 ) ) ) ) “ { ℎ } )
49 nfv ⊢ Ⅎ 𝑏 ∩ ( ◡ 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 𝑔 ) ) ) ) “ { ℎ } )
50 nfmpt1 ⊢ Ⅎ 𝑔 ( 𝑔 ∈ V ↦ ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) )
51 50 nfrecs ⊢ Ⅎ 𝑔 recs ( ( 𝑔 ∈ V ↦ ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) ) )
52 51 nfcnv ⊢ Ⅎ 𝑔 ◡ recs ( ( 𝑔 ∈ V ↦ ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) ) )
53 nfcv ⊢ Ⅎ 𝑔 { 𝑐 }
54 52 53 nfima ⊢ Ⅎ 𝑔 ( ◡ recs ( ( 𝑔 ∈ V ↦ ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) ) ) “ { 𝑐 } )
55 54 nfint ⊢ Ⅎ 𝑔 ∩ ( ◡ recs ( ( 𝑔 ∈ V ↦ ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) ) ) “ { 𝑐 } )
56 nfcv ⊢ Ⅎ 𝑔 { 𝑏 }
57 52 56 nfima ⊢ Ⅎ 𝑔 ( ◡ recs ( ( 𝑔 ∈ V ↦ ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) ) ) “ { 𝑏 } )
58 57 nfint ⊢ Ⅎ 𝑔 ∩ ( ◡ recs ( ( 𝑔 ∈ V ↦ ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) ) ) “ { 𝑏 } )
59 55 58 nfel ⊢ Ⅎ 𝑔 ∩ ( ◡ 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 𝑔 ) ) ) ) “ { 𝑏 } )
60 nfcv ⊢ Ⅎ ℎ V
61 nfcv ⊢ Ⅎ ℎ ( 𝑦 ‘ 𝑔 )
62 nfcv ⊢ Ⅎ ℎ ( 𝑅1 ‘ dom 𝑒 )
63 nfopab2 ⊢ Ⅎ ℎ { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) }
64 61 62 63 nfsup ⊢ Ⅎ ℎ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } )
65 60 64 nfmpt ⊢ Ⅎ ℎ ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) )
66 nfcv ⊢ Ⅎ ℎ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 )
67 65 66 nffv ⊢ Ⅎ ℎ ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) )
68 60 67 nfmpt ⊢ Ⅎ ℎ ( 𝑔 ∈ V ↦ ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) )
69 68 nfrecs ⊢ Ⅎ ℎ recs ( ( 𝑔 ∈ V ↦ ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) ) )
70 69 nfcnv ⊢ Ⅎ ℎ ◡ recs ( ( 𝑔 ∈ V ↦ ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) ) )
71 nfcv ⊢ Ⅎ ℎ { 𝑐 }
72 70 71 nfima ⊢ Ⅎ ℎ ( ◡ recs ( ( 𝑔 ∈ V ↦ ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) ) ) “ { 𝑐 } )
73 72 nfint ⊢ Ⅎ ℎ ∩ ( ◡ recs ( ( 𝑔 ∈ V ↦ ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) ) ) “ { 𝑐 } )
74 nfcv ⊢ Ⅎ ℎ { 𝑏 }
75 70 74 nfima ⊢ Ⅎ ℎ ( ◡ recs ( ( 𝑔 ∈ V ↦ ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) ) ) “ { 𝑏 } )
76 75 nfint ⊢ Ⅎ ℎ ∩ ( ◡ recs ( ( 𝑔 ∈ V ↦ ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) ) ) “ { 𝑏 } )
77 73 76 nfel ⊢ Ⅎ ℎ ∩ ( ◡ 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 𝑔 ) ) ) ) “ { 𝑏 } )
78 sneq ⊢ ( 𝑔 = 𝑐 → { 𝑔 } = { 𝑐 } )
79 78 imaeq2d ⊢ ( 𝑔 = 𝑐 → ( ◡ 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 𝑔 ) ) ) ) “ { 𝑐 } ) )
80 79 inteqd ⊢ ( 𝑔 = 𝑐 → ∩ ( ◡ 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 𝑔 ) ) ) ) “ { 𝑐 } ) )
81 sneq ⊢ ( ℎ = 𝑏 → { ℎ } = { 𝑏 } )
82 81 imaeq2d ⊢ ( ℎ = 𝑏 → ( ◡ 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 𝑔 ) ) ) ) “ { 𝑏 } ) )
83 82 inteqd ⊢ ( ℎ = 𝑏 → ∩ ( ◡ 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 𝑔 ) ) ) ) “ { 𝑏 } ) )
84 eleq12 ⊢ ( ( ∩ ( ◡ 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 𝑔 ) ) ) ) “ { 𝑏 } ) ) )
85 80 83 84 syl2an ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → ( ∩ ( ◡ 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 𝑔 ) ) ) ) “ { 𝑏 } ) ) )
86 48 49 59 77 85 cbvopab ⊢ { ⟨ 𝑔 , ℎ ⟩ ∣ ∩ ( ◡ 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 𝑔 ) ) ) ) “ { 𝑏 } ) }
87 fveq2 ⊢ ( 𝑔 = 𝑐 → ( rank ‘ 𝑔 ) = ( rank ‘ 𝑐 ) )
88 fveq2 ⊢ ( ℎ = 𝑏 → ( rank ‘ ℎ ) = ( rank ‘ 𝑏 ) )
89 87 88 breqan12d ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → ( ( rank ‘ 𝑔 ) E ( rank ‘ ℎ ) ↔ ( rank ‘ 𝑐 ) E ( rank ‘ 𝑏 ) ) )
90 87 88 eqeqan12d ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → ( ( rank ‘ 𝑔 ) = ( rank ‘ ℎ ) ↔ ( rank ‘ 𝑐 ) = ( rank ‘ 𝑏 ) ) )
91 simpl ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → 𝑔 = 𝑐 )
92 suceq ⊢ ( ( rank ‘ 𝑔 ) = ( rank ‘ 𝑐 ) → suc ( rank ‘ 𝑔 ) = suc ( rank ‘ 𝑐 ) )
93 87 92 syl ⊢ ( 𝑔 = 𝑐 → suc ( rank ‘ 𝑔 ) = suc ( rank ‘ 𝑐 ) )
94 93 adantr ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → suc ( rank ‘ 𝑔 ) = suc ( rank ‘ 𝑐 ) )
95 94 fveq2d ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → ( 𝑒 ‘ suc ( rank ‘ 𝑔 ) ) = ( 𝑒 ‘ suc ( rank ‘ 𝑐 ) ) )
96 simpr ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → ℎ = 𝑏 )
97 91 95 96 breq123d ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → ( 𝑔 ( 𝑒 ‘ suc ( rank ‘ 𝑔 ) ) ℎ ↔ 𝑐 ( 𝑒 ‘ suc ( rank ‘ 𝑐 ) ) 𝑏 ) )
98 90 97 anbi12d ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → ( ( ( rank ‘ 𝑔 ) = ( rank ‘ ℎ ) ∧ 𝑔 ( 𝑒 ‘ suc ( rank ‘ 𝑔 ) ) ℎ ) ↔ ( ( rank ‘ 𝑐 ) = ( rank ‘ 𝑏 ) ∧ 𝑐 ( 𝑒 ‘ suc ( rank ‘ 𝑐 ) ) 𝑏 ) ) )
99 89 98 orbi12d ⊢ ( ( 𝑔 = 𝑐 ∧ ℎ = 𝑏 ) → ( ( ( rank ‘ 𝑔 ) E ( rank ‘ ℎ ) ∨ ( ( rank ‘ 𝑔 ) = ( rank ‘ ℎ ) ∧ 𝑔 ( 𝑒 ‘ suc ( rank ‘ 𝑔 ) ) ℎ ) ) ↔ ( ( rank ‘ 𝑐 ) E ( rank ‘ 𝑏 ) ∨ ( ( rank ‘ 𝑐 ) = ( rank ‘ 𝑏 ) ∧ 𝑐 ( 𝑒 ‘ suc ( rank ‘ 𝑐 ) ) 𝑏 ) ) ) )
100 99 cbvopabv ⊢ { ⟨ 𝑔 , ℎ ⟩ ∣ ( ( rank ‘ 𝑔 ) E ( rank ‘ ℎ ) ∨ ( ( rank ‘ 𝑔 ) = ( rank ‘ ℎ ) ∧ 𝑔 ( 𝑒 ‘ suc ( rank ‘ 𝑔 ) ) ℎ ) ) } = { ⟨ 𝑐 , 𝑏 ⟩ ∣ ( ( rank ‘ 𝑐 ) E ( rank ‘ 𝑏 ) ∨ ( ( rank ‘ 𝑐 ) = ( rank ‘ 𝑏 ) ∧ 𝑐 ( 𝑒 ‘ suc ( rank ‘ 𝑐 ) ) 𝑏 ) ) }
101 eqid ⊢ ( 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 𝑒 ) ) )
102 dmeq ⊢ ( 𝑙 = 𝑒 → dom 𝑙 = dom 𝑒 )
103 102 unieqd ⊢ ( 𝑙 = 𝑒 → ∪ dom 𝑙 = ∪ dom 𝑒 )
104 102 103 eqeq12d ⊢ ( 𝑙 = 𝑒 → ( dom 𝑙 = ∪ dom 𝑙 ↔ dom 𝑒 = ∪ dom 𝑒 ) )
105 fveq1 ⊢ ( 𝑙 = 𝑒 → ( 𝑙 ‘ suc ( rank ‘ 𝑔 ) ) = ( 𝑒 ‘ suc ( rank ‘ 𝑔 ) ) )
106 105 breqd ⊢ ( 𝑙 = 𝑒 → ( 𝑔 ( 𝑙 ‘ suc ( rank ‘ 𝑔 ) ) ℎ ↔ 𝑔 ( 𝑒 ‘ suc ( rank ‘ 𝑔 ) ) ℎ ) )
107 106 anbi2d ⊢ ( 𝑙 = 𝑒 → ( ( ( rank ‘ 𝑔 ) = ( rank ‘ ℎ ) ∧ 𝑔 ( 𝑙 ‘ suc ( rank ‘ 𝑔 ) ) ℎ ) ↔ ( ( rank ‘ 𝑔 ) = ( rank ‘ ℎ ) ∧ 𝑔 ( 𝑒 ‘ suc ( rank ‘ 𝑔 ) ) ℎ ) ) )
108 107 orbi2d ⊢ ( 𝑙 = 𝑒 → ( ( ( rank ‘ 𝑔 ) E ( rank ‘ ℎ ) ∨ ( ( rank ‘ 𝑔 ) = ( rank ‘ ℎ ) ∧ 𝑔 ( 𝑙 ‘ suc ( rank ‘ 𝑔 ) ) ℎ ) ) ↔ ( ( rank ‘ 𝑔 ) E ( rank ‘ ℎ ) ∨ ( ( rank ‘ 𝑔 ) = ( rank ‘ ℎ ) ∧ 𝑔 ( 𝑒 ‘ suc ( rank ‘ 𝑔 ) ) ℎ ) ) ) )
109 108 opabbidv ⊢ ( 𝑙 = 𝑒 → { ⟨ 𝑔 , ℎ ⟩ ∣ ( ( rank ‘ 𝑔 ) E ( rank ‘ ℎ ) ∨ ( ( rank ‘ 𝑔 ) = ( rank ‘ ℎ ) ∧ 𝑔 ( 𝑙 ‘ suc ( rank ‘ 𝑔 ) ) ℎ ) ) } = { ⟨ 𝑔 , ℎ ⟩ ∣ ( ( rank ‘ 𝑔 ) E ( rank ‘ ℎ ) ∨ ( ( rank ‘ 𝑔 ) = ( rank ‘ ℎ ) ∧ 𝑔 ( 𝑒 ‘ suc ( rank ‘ 𝑔 ) ) ℎ ) ) } )
110 eqidd ⊢ ( 𝑙 = 𝑒 → ( 𝑦 ‘ 𝑔 ) = ( 𝑦 ‘ 𝑔 ) )
111 102 fveq2d ⊢ ( 𝑙 = 𝑒 → ( 𝑅1 ‘ dom 𝑙 ) = ( 𝑅1 ‘ dom 𝑒 ) )
112 103 fveq2d ⊢ ( 𝑙 = 𝑒 → ( 𝑅1 ‘ ∪ dom 𝑙 ) = ( 𝑅1 ‘ ∪ dom 𝑒 ) )
113 id ⊢ ( 𝑙 = 𝑒 → 𝑙 = 𝑒 )
114 113 103 fveq12d ⊢ ( 𝑙 = 𝑒 → ( 𝑙 ‘ ∪ dom 𝑙 ) = ( 𝑒 ‘ ∪ dom 𝑒 ) )
115 114 breqd ⊢ ( 𝑙 = 𝑒 → ( 𝑗 ( 𝑙 ‘ ∪ dom 𝑙 ) 𝑖 ↔ 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 ) )
116 115 imbi1d ⊢ ( 𝑙 = 𝑒 → ( ( 𝑗 ( 𝑙 ‘ ∪ dom 𝑙 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ↔ ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) )
117 112 116 raleqbidv ⊢ ( 𝑙 = 𝑒 → ( ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑙 ) ( 𝑗 ( 𝑙 ‘ ∪ dom 𝑙 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ↔ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) )
118 117 anbi2d ⊢ ( 𝑙 = 𝑒 → ( ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑙 ) ( 𝑗 ( 𝑙 ‘ ∪ dom 𝑙 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) ↔ ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) ) )
119 112 118 rexeqbidv ⊢ ( 𝑙 = 𝑒 → ( ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑙 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑙 ) ( 𝑗 ( 𝑙 ‘ ∪ dom 𝑙 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) ↔ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) ) )
120 119 opabbidv ⊢ ( 𝑙 = 𝑒 → { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑙 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑙 ) ( 𝑗 ( 𝑙 ‘ ∪ dom 𝑙 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } = { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } )
121 110 111 120 supeq123d ⊢ ( 𝑙 = 𝑒 → sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑙 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑙 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑙 ) ( 𝑗 ( 𝑙 ‘ ∪ dom 𝑙 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) = sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) )
122 121 mpteq2dv ⊢ ( 𝑙 = 𝑒 → ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑙 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑙 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑙 ) ( 𝑗 ( 𝑙 ‘ ∪ dom 𝑙 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) = ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) )
123 111 difeq1d ⊢ ( 𝑙 = 𝑒 → ( ( 𝑅1 ‘ dom 𝑙 ) ∖ ran 𝑔 ) = ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) )
124 122 123 fveq12d ⊢ ( 𝑙 = 𝑒 → ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑙 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑙 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑙 ) ( 𝑗 ( 𝑙 ‘ ∪ dom 𝑙 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑙 ) ∖ ran 𝑔 ) ) = ( ( 𝑔 ∈ V ↦ sup ( ( 𝑦 ‘ 𝑔 ) , ( 𝑅1 ‘ dom 𝑒 ) , { ⟨ 𝑔 , ℎ ⟩ ∣ ∃ 𝑖 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( ( 𝑖 ∈ ℎ ∧ ¬ 𝑖 ∈ 𝑔 ) ∧ ∀ 𝑗 ∈ ( 𝑅1 ‘ ∪ dom 𝑒 ) ( 𝑗 ( 𝑒 ‘ ∪ dom 𝑒 ) 𝑖 → ( 𝑗 ∈ 𝑔 ↔ 𝑗 ∈ ℎ ) ) ) } ) ) ‘ ( ( 𝑅1 ‘ dom 𝑒 ) ∖ ran 𝑔 ) ) )
125 124 mpteq2dv ⊢ ( 𝑙 = 𝑒 → ( 𝑔 ∈ 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 𝑔 ) ) ) )
126 recseq ⊢ ( ( 𝑔 ∈ 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 𝑔 ) ) ) ) )
127 125 126 syl ⊢ ( 𝑙 = 𝑒 → 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 𝑔 ) ) ) ) )
128 127 cnveqd ⊢ ( 𝑙 = 𝑒 → ◡ 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 𝑔 ) ) ) ) )
129 128 imaeq1d ⊢ ( 𝑙 = 𝑒 → ( ◡ 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 𝑔 ) ) ) ) “ { 𝑔 } ) )
130 129 inteqd ⊢ ( 𝑙 = 𝑒 → ∩ ( ◡ 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 𝑔 ) ) ) ) “ { 𝑔 } ) )
131 128 imaeq1d ⊢ ( 𝑙 = 𝑒 → ( ◡ 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 𝑔 ) ) ) ) “ { ℎ } ) )
132 131 inteqd ⊢ ( 𝑙 = 𝑒 → ∩ ( ◡ 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 𝑔 ) ) ) ) “ { ℎ } ) )
133 130 132 eleq12d ⊢ ( 𝑙 = 𝑒 → ( ∩ ( ◡ 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 𝑔 ) ) ) ) “ { ℎ } ) ) )
134 133 opabbidv ⊢ ( 𝑙 = 𝑒 → { ⟨ 𝑔 , ℎ ⟩ ∣ ∩ ( ◡ 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 𝑔 ) ) ) ) “ { ℎ } ) } )
135 104 109 134 ifbieq12d ⊢ ( 𝑙 = 𝑒 → 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 𝑔 ) ) ) ) “ { ℎ } ) } ) )
136 111 sqxpeqd ⊢ ( 𝑙 = 𝑒 → ( ( 𝑅1 ‘ dom 𝑙 ) × ( 𝑅1 ‘ dom 𝑙 ) ) = ( ( 𝑅1 ‘ dom 𝑒 ) × ( 𝑅1 ‘ dom 𝑒 ) ) )
137 135 136 ineq12d ⊢ ( 𝑙 = 𝑒 → ( 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 𝑒 ) ) ) )
138 137 cbvmptv ⊢ ( 𝑙 ∈ 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 𝑒 ) ) ) )
139 recseq ⊢ ( ( 𝑙 ∈ 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 𝑒 ) ) ) ) ) )
140 138 139 ax-mp ⊢ 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 𝑒 ) ) ) ) )
141 neeq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 ≠ ∅ ↔ 𝑐 ≠ ∅ ) )
142 fveq2 ⊢ ( 𝑎 = 𝑐 → ( 𝑦 ‘ 𝑎 ) = ( 𝑦 ‘ 𝑐 ) )
143 pweq ⊢ ( 𝑎 = 𝑐 → 𝒫 𝑎 = 𝒫 𝑐 )
144 143 ineq1d ⊢ ( 𝑎 = 𝑐 → ( 𝒫 𝑎 ∩ Fin ) = ( 𝒫 𝑐 ∩ Fin ) )
145 144 difeq1d ⊢ ( 𝑎 = 𝑐 → ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) = ( ( 𝒫 𝑐 ∩ Fin ) ∖ { ∅ } ) )
146 142 145 eleq12d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ↔ ( 𝑦 ‘ 𝑐 ) ∈ ( ( 𝒫 𝑐 ∩ Fin ) ∖ { ∅ } ) ) )
147 141 146 imbi12d ⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) ↔ ( 𝑐 ≠ ∅ → ( 𝑦 ‘ 𝑐 ) ∈ ( ( 𝒫 𝑐 ∩ Fin ) ∖ { ∅ } ) ) ) )
148 147 cbvralvw ⊢ ( ∀ 𝑎 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑎 ≠ ∅ → ( 𝑦 ‘ 𝑎 ) ∈ ( ( 𝒫 𝑎 ∩ Fin ) ∖ { ∅ } ) ) ↔ ∀ 𝑐 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑐 ≠ ∅ → ( 𝑦 ‘ 𝑐 ) ∈ ( ( 𝒫 𝑐 ∩ Fin ) ∖ { ∅ } ) ) )
149 2 148 sylib ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝒫 ( 𝑅1 ‘ 𝐴 ) ( 𝑐 ≠ ∅ → ( 𝑦 ‘ 𝑐 ) ∈ ( ( 𝒫 𝑐 ∩ Fin ) ∖ { ∅ } ) ) )
150 31 39 47 86 100 101 140 1 149 aomclem7 ⊢ ( 𝜑 → ∃ 𝑏 𝑏 We ( 𝑅1 ‘ 𝐴 ) )