| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | satfbrsuc.s | . . . . . 6
⊢ 𝑆 = (𝑀 Sat 𝐸) | 
| 2 | 1 | satfvsuc 35367 | . . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → (𝑆‘suc 𝑁) = ((𝑆‘𝑁) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})) | 
| 3 | 2 | 3expa 1118 | . . . 4
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑁 ∈ ω) → (𝑆‘suc 𝑁) = ((𝑆‘𝑁) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})) | 
| 4 | 3 | 3adant3 1132 | . . 3
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑁 ∈ ω ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝑆‘suc 𝑁) = ((𝑆‘𝑁) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})) | 
| 5 | 4 | breqd 5153 | . 2
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑁 ∈ ω ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴(𝑆‘suc 𝑁)𝐵 ↔ 𝐴((𝑆‘𝑁) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})𝐵)) | 
| 6 |  | brun 5193 | . . . 4
⊢ (𝐴((𝑆‘𝑁) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})𝐵 ↔ (𝐴(𝑆‘𝑁)𝐵 ∨ 𝐴{〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}𝐵)) | 
| 7 |  | satfbrsuc.p | . . . . . . . 8
⊢ 𝑃 = (𝑆‘𝑁) | 
| 8 | 7 | eqcomi 2745 | . . . . . . 7
⊢ (𝑆‘𝑁) = 𝑃 | 
| 9 | 8 | breqi 5148 | . . . . . 6
⊢ (𝐴(𝑆‘𝑁)𝐵 ↔ 𝐴𝑃𝐵) | 
| 10 | 9 | a1i 11 | . . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴(𝑆‘𝑁)𝐵 ↔ 𝐴𝑃𝐵)) | 
| 11 |  | eqeq1 2740 | . . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔ 𝐴 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) | 
| 12 |  | eqeq1 2740 | . . . . . . . . . 10
⊢ (𝑦 = 𝐵 → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) ↔ 𝐵 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))))) | 
| 13 | 11, 12 | bi2anan9 638 | . . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ↔ (𝐴 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝐵 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))))) | 
| 14 | 13 | rexbidv 3178 | . . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑣 ∈ 𝑃 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ↔ ∃𝑣 ∈ 𝑃 (𝐴 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝐵 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))))) | 
| 15 |  | eqeq1 2740 | . . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ 𝐴 = ∀𝑔𝑖(1st ‘𝑢))) | 
| 16 |  | eqeq1 2740 | . . . . . . . . . 10
⊢ (𝑦 = 𝐵 → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ↔ 𝐵 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) | 
| 17 | 15, 16 | bi2anan9 638 | . . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) ↔ (𝐴 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝐵 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))) | 
| 18 | 17 | rexbidv 3178 | . . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) ↔ ∃𝑖 ∈ ω (𝐴 =
∀𝑔𝑖(1st ‘𝑢) ∧ 𝐵 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))) | 
| 19 | 14, 18 | orbi12d 918 | . . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ((∃𝑣 ∈ 𝑃 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ (∃𝑣 ∈ 𝑃 (𝐴 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝐵 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝐴 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝐵 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))) | 
| 20 | 19 | rexbidv 3178 | . . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑢 ∈ 𝑃 (∃𝑣 ∈ 𝑃 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ ∃𝑢 ∈ 𝑃 (∃𝑣 ∈ 𝑃 (𝐴 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝐵 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝐴 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝐵 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))) | 
| 21 | 8 | rexeqi 3324 | . . . . . . . . 9
⊢
(∃𝑣 ∈
(𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ↔ ∃𝑣 ∈ 𝑃 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))))) | 
| 22 | 21 | orbi1i 913 | . . . . . . . 8
⊢
((∃𝑣 ∈
(𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ (∃𝑣 ∈ 𝑃 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))) | 
| 23 | 8, 22 | rexeqbii 3344 | . . . . . . 7
⊢
(∃𝑢 ∈
(𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ ∃𝑢 ∈ 𝑃 (∃𝑣 ∈ 𝑃 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))) | 
| 24 | 23 | opabbii 5209 | . . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} = {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ 𝑃 (∃𝑣 ∈ 𝑃 (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} | 
| 25 | 20, 24 | brabga 5538 | . . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴{〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}𝐵 ↔ ∃𝑢 ∈ 𝑃 (∃𝑣 ∈ 𝑃 (𝐴 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝐵 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝐴 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝐵 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))) | 
| 26 | 10, 25 | orbi12d 918 | . . . 4
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝐴(𝑆‘𝑁)𝐵 ∨ 𝐴{〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}𝐵) ↔ (𝐴𝑃𝐵 ∨ ∃𝑢 ∈ 𝑃 (∃𝑣 ∈ 𝑃 (𝐴 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝐵 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝐴 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝐵 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))) | 
| 27 | 6, 26 | bitrid 283 | . . 3
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴((𝑆‘𝑁) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})𝐵 ↔ (𝐴𝑃𝐵 ∨ ∃𝑢 ∈ 𝑃 (∃𝑣 ∈ 𝑃 (𝐴 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝐵 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝐴 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝐵 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))) | 
| 28 | 27 | 3ad2ant3 1135 | . 2
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑁 ∈ ω ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴((𝑆‘𝑁) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))})𝐵 ↔ (𝐴𝑃𝐵 ∨ ∃𝑢 ∈ 𝑃 (∃𝑣 ∈ 𝑃 (𝐴 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝐵 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝐴 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝐵 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))) | 
| 29 | 5, 28 | bitrd 279 | 1
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ 𝑁 ∈ ω ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐴(𝑆‘suc 𝑁)𝐵 ↔ (𝐴𝑃𝐵 ∨ ∃𝑢 ∈ 𝑃 (∃𝑣 ∈ 𝑃 (𝐴 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝐵 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝐴 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝐵 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))))) |