| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl 482 | . . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → 𝑀 ∈ 𝑉) | 
| 2 |  | simpr 484 | . . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → 𝐸 ∈ 𝑊) | 
| 3 |  | 1onn 8679 | . . . . . 6
⊢
1o ∈ ω | 
| 4 | 3 | a1i 11 | . . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → 1o ∈
ω) | 
| 5 | 1, 2, 4 | 3jca 1128 | . . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 1o ∈
ω)) | 
| 6 | 5 | 3ad2ant1 1133 | . . 3
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 1o ∈
ω)) | 
| 7 |  | satffun 35415 | . . 3
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 1o ∈ ω) →
Fun ((𝑀 Sat 𝐸)‘1o)) | 
| 8 | 6, 7 | syl 17 | . 2
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → Fun ((𝑀 Sat 𝐸)‘1o)) | 
| 9 |  | simp2l 1199 | . . . . . . 7
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝐼 ∈ ω) | 
| 10 |  | simp2r 1200 | . . . . . . 7
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝐽 ∈ ω) | 
| 11 |  | simp3l 1201 | . . . . . . . . 9
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝐾 ∈ ω) | 
| 12 |  | simp3r 1202 | . . . . . . . . 9
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝐿 ∈ ω) | 
| 13 |  | satfv1fvfmla1.x | . . . . . . . . . . 11
⊢ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿)) | 
| 14 |  | eqid 2736 | . . . . . . . . . . 11
⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} | 
| 15 | 13, 14 | pm3.2i 470 | . . . . . . . . . 10
⊢ (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}) | 
| 16 | 15 | a1i 11 | . . . . . . . . 9
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))})) | 
| 17 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝐾 → (𝑘∈𝑔𝑙) = (𝐾∈𝑔𝑙)) | 
| 18 | 17 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑙)) = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑙))) | 
| 19 | 18 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑙)) ↔ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑙)))) | 
| 20 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝐾 → (𝑎‘𝑘) = (𝑎‘𝐾)) | 
| 21 | 20 | breq1d 5152 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝐾 → ((𝑎‘𝑘)𝐸(𝑎‘𝑙) ↔ (𝑎‘𝐾)𝐸(𝑎‘𝑙))) | 
| 22 | 21 | notbid 318 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝐾 → (¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙) ↔ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝑙))) | 
| 23 | 22 | orbi2d 915 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝐾 → ((¬ (𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙)) ↔ (¬ (𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝑙)))) | 
| 24 | 23 | rabbidv 3443 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝑙))}) | 
| 25 | 24 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → ({𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝑙))})) | 
| 26 | 19, 25 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → ((𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ↔ (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝑙))}))) | 
| 27 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑙 = 𝐿 → (𝐾∈𝑔𝑙) = (𝐾∈𝑔𝐿)) | 
| 28 | 27 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑙 = 𝐿 → ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑙)) = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿))) | 
| 29 | 28 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑙 = 𝐿 → (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑙)) ↔ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿)))) | 
| 30 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝐿 → (𝑎‘𝑙) = (𝑎‘𝐿)) | 
| 31 | 30 | breq2d 5154 | . . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝐿 → ((𝑎‘𝐾)𝐸(𝑎‘𝑙) ↔ (𝑎‘𝐾)𝐸(𝑎‘𝐿))) | 
| 32 | 31 | notbid 318 | . . . . . . . . . . . . . 14
⊢ (𝑙 = 𝐿 → (¬ (𝑎‘𝐾)𝐸(𝑎‘𝑙) ↔ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))) | 
| 33 | 32 | orbi2d 915 | . . . . . . . . . . . . 13
⊢ (𝑙 = 𝐿 → ((¬ (𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝑙)) ↔ (¬ (𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿)))) | 
| 34 | 33 | rabbidv 3443 | . . . . . . . . . . . 12
⊢ (𝑙 = 𝐿 → {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝑙))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}) | 
| 35 | 34 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑙 = 𝐿 → ({𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝑙))} ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))})) | 
| 36 | 29, 35 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑙 = 𝐿 → ((𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝑙))}) ↔ (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}))) | 
| 37 | 26, 36 | rspc2ev 3634 | . . . . . . . . 9
⊢ ((𝐾 ∈ ω ∧ 𝐿 ∈ ω ∧ (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))})) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})) | 
| 38 | 11, 12, 16, 37 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})) | 
| 39 | 38 | orcd 873 | . . . . . . 7
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝐼∈𝑔𝐽) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝐽 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))}))) | 
| 40 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝐼 → (𝑖∈𝑔𝑗) = (𝐼∈𝑔𝑗)) | 
| 41 | 40 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙))) | 
| 42 | 41 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → (𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ↔ 𝑋 = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)))) | 
| 43 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝐼 → (𝑎‘𝑖) = (𝑎‘𝐼)) | 
| 44 | 43 | breq1d 5152 | . . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝐼 → ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ↔ (𝑎‘𝐼)𝐸(𝑎‘𝑗))) | 
| 45 | 44 | notbid 318 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝐼 → (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ↔ ¬ (𝑎‘𝐼)𝐸(𝑎‘𝑗))) | 
| 46 | 45 | orbi1d 916 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝐼 → ((¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙)) ↔ (¬ (𝑎‘𝐼)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙)))) | 
| 47 | 46 | rabbidv 3443 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) | 
| 48 | 47 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → ({𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})) | 
| 49 | 42, 48 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑖 = 𝐼 → ((𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ↔ (𝑋 = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))) | 
| 50 | 49 | 2rexbidv 3221 | . . . . . . . . 9
⊢ (𝑖 = 𝐼 → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))) | 
| 51 |  | eqidd 2737 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝐼 → 𝑛 = 𝑛) | 
| 52 | 51, 40 | goaleq12d 35357 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → ∀𝑔𝑛(𝑖∈𝑔𝑗) = ∀𝑔𝑛(𝐼∈𝑔𝑗)) | 
| 53 | 52 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → (𝑋 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ↔ 𝑋 = ∀𝑔𝑛(𝐼∈𝑔𝑗))) | 
| 54 |  | eqeq1 2740 | . . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝐼 → (𝑖 = 𝑛 ↔ 𝐼 = 𝑛)) | 
| 55 |  | biidd 262 | . . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝐼 → (if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)) ↔ if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)))) | 
| 56 | 43 | breq1d 5152 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝐼 → ((𝑎‘𝑖)𝐸𝑧 ↔ (𝑎‘𝐼)𝐸𝑧)) | 
| 57 | 56, 44 | ifpbi23d 1079 | . . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝐼 → (if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)) ↔ if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗)))) | 
| 58 | 54, 55, 57 | ifpbi123d 1078 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝐼 → (if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗))) ↔ if-(𝐼 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗))))) | 
| 59 | 58 | ralbidv 3177 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝐼 → (∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗))) ↔ ∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗))))) | 
| 60 | 59 | rabbidv 3443 | . . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗)))}) | 
| 61 | 60 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → ({𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗)))})) | 
| 62 | 53, 61 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑖 = 𝐼 → ((𝑋 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) ↔ (𝑋 = ∀𝑔𝑛(𝐼∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗)))}))) | 
| 63 | 62 | rexbidv 3178 | . . . . . . . . 9
⊢ (𝑖 = 𝐼 → (∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) ↔ ∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝐼∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗)))}))) | 
| 64 | 50, 63 | orbi12d 918 | . . . . . . . 8
⊢ (𝑖 = 𝐼 → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝐼∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗)))})))) | 
| 65 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑗 = 𝐽 → (𝐼∈𝑔𝑗) = (𝐼∈𝑔𝐽)) | 
| 66 | 65 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (𝑗 = 𝐽 → ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑙))) | 
| 67 | 66 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑗 = 𝐽 → (𝑋 = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ↔ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑙)))) | 
| 68 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝐽 → (𝑎‘𝑗) = (𝑎‘𝐽)) | 
| 69 | 68 | breq2d 5154 | . . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝐽 → ((𝑎‘𝐼)𝐸(𝑎‘𝑗) ↔ (𝑎‘𝐼)𝐸(𝑎‘𝐽))) | 
| 70 | 69 | notbid 318 | . . . . . . . . . . . . . 14
⊢ (𝑗 = 𝐽 → (¬ (𝑎‘𝐼)𝐸(𝑎‘𝑗) ↔ ¬ (𝑎‘𝐼)𝐸(𝑎‘𝐽))) | 
| 71 | 70 | orbi1d 916 | . . . . . . . . . . . . 13
⊢ (𝑗 = 𝐽 → ((¬ (𝑎‘𝐼)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙)) ↔ (¬ (𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙)))) | 
| 72 | 71 | rabbidv 3443 | . . . . . . . . . . . 12
⊢ (𝑗 = 𝐽 → {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) | 
| 73 | 72 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑗 = 𝐽 → ({𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})) | 
| 74 | 67, 73 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑗 = 𝐽 → ((𝑋 = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ↔ (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))) | 
| 75 | 74 | 2rexbidv 3221 | . . . . . . . . 9
⊢ (𝑗 = 𝐽 → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))) | 
| 76 |  | eqidd 2737 | . . . . . . . . . . . . 13
⊢ (𝑗 = 𝐽 → 𝑛 = 𝑛) | 
| 77 | 76, 65 | goaleq12d 35357 | . . . . . . . . . . . 12
⊢ (𝑗 = 𝐽 → ∀𝑔𝑛(𝐼∈𝑔𝑗) = ∀𝑔𝑛(𝐼∈𝑔𝐽)) | 
| 78 | 77 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑗 = 𝐽 → (𝑋 = ∀𝑔𝑛(𝐼∈𝑔𝑗) ↔ 𝑋 = ∀𝑔𝑛(𝐼∈𝑔𝐽))) | 
| 79 |  | eqeq1 2740 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝐽 → (𝑗 = 𝑛 ↔ 𝐽 = 𝑛)) | 
| 80 |  | biidd 262 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝐽 → (𝑧𝐸𝑧 ↔ 𝑧𝐸𝑧)) | 
| 81 | 68 | breq2d 5154 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝐽 → (𝑧𝐸(𝑎‘𝑗) ↔ 𝑧𝐸(𝑎‘𝐽))) | 
| 82 | 79, 80, 81 | ifpbi123d 1078 | . . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝐽 → (if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)) ↔ if-(𝐽 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)))) | 
| 83 |  | biidd 262 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝐽 → ((𝑎‘𝐼)𝐸𝑧 ↔ (𝑎‘𝐼)𝐸𝑧)) | 
| 84 | 79, 83, 69 | ifpbi123d 1078 | . . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝐽 → (if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗)) ↔ if-(𝐽 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))) | 
| 85 | 82, 84 | ifpbi23d 1079 | . . . . . . . . . . . . . 14
⊢ (𝑗 = 𝐽 → (if-(𝐼 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗))) ↔ if-(𝐼 = 𝑛, if-(𝐽 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽))))) | 
| 86 | 85 | ralbidv 3177 | . . . . . . . . . . . . 13
⊢ (𝑗 = 𝐽 → (∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗))) ↔ ∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝐽 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽))))) | 
| 87 | 86 | rabbidv 3443 | . . . . . . . . . . . 12
⊢ (𝑗 = 𝐽 → {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗)))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝐽 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))}) | 
| 88 | 87 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑗 = 𝐽 → ({𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗)))} ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝐽 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))})) | 
| 89 | 78, 88 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑗 = 𝐽 → ((𝑋 = ∀𝑔𝑛(𝐼∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗)))}) ↔ (𝑋 = ∀𝑔𝑛(𝐼∈𝑔𝐽) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝐽 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))}))) | 
| 90 | 89 | rexbidv 3178 | . . . . . . . . 9
⊢ (𝑗 = 𝐽 → (∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝐼∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗)))}) ↔ ∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝐼∈𝑔𝐽) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝐽 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))}))) | 
| 91 | 75, 90 | orbi12d 918 | . . . . . . . 8
⊢ (𝑗 = 𝐽 → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝐼∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝑗)))})) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝐼∈𝑔𝐽) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝐽 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))})))) | 
| 92 | 64, 91 | rspc2ev 3634 | . . . . . . 7
⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧
(∃𝑘 ∈ ω
∃𝑙 ∈ ω
(𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝐼∈𝑔𝐽) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑛, if-(𝐽 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑛, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) | 
| 93 | 9, 10, 39, 92 | syl3anc 1372 | . . . . . 6
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) | 
| 94 | 13 | ovexi 7466 | . . . . . . . 8
⊢ 𝑋 ∈ V | 
| 95 | 94 | a1i 11 | . . . . . . 7
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝑋 ∈ V) | 
| 96 |  | ovex 7465 | . . . . . . . 8
⊢ (𝑀 ↑m ω)
∈ V | 
| 97 | 96 | rabex 5338 | . . . . . . 7
⊢ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} ∈ V | 
| 98 |  | eqeq1 2740 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ↔ 𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)))) | 
| 99 |  | eqeq1 2740 | . . . . . . . . . . . 12
⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})) | 
| 100 | 98, 99 | bi2anan9 638 | . . . . . . . . . . 11
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}) → ((𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ↔ (𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))) | 
| 101 | 100 | 2rexbidv 3221 | . . . . . . . . . 10
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))) | 
| 102 |  | eqeq1 2740 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ↔ 𝑋 = ∀𝑔𝑛(𝑖∈𝑔𝑗))) | 
| 103 |  | eqeq1 2740 | . . . . . . . . . . . 12
⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) | 
| 104 | 102, 103 | bi2anan9 638 | . . . . . . . . . . 11
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}) → ((𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) ↔ (𝑋 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) | 
| 105 | 104 | rexbidv 3178 | . . . . . . . . . 10
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}) → (∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) ↔ ∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) | 
| 106 | 101, 105 | orbi12d 918 | . . . . . . . . 9
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}) → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))) | 
| 107 | 106 | 2rexbidv 3221 | . . . . . . . 8
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))) | 
| 108 | 107 | opelopabga 5537 | . . . . . . 7
⊢ ((𝑋 ∈ V ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} ∈ V) → (〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}〉 ∈ {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))} ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))) | 
| 109 | 95, 97, 108 | sylancl 586 | . . . . . 6
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}〉 ∈ {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))} ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑋 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))) | 
| 110 | 93, 109 | mpbird 257 | . . . . 5
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}〉 ∈ {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))}) | 
| 111 | 110 | olcd 874 | . . . 4
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}〉 ∈ ((𝑀 Sat 𝐸)‘∅) ∨ 〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}〉 ∈ {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))})) | 
| 112 |  | elun 4152 | . . . 4
⊢
(〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}〉 ∈ (((𝑀 Sat 𝐸)‘∅) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))}) ↔ (〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}〉 ∈ ((𝑀 Sat 𝐸)‘∅) ∨ 〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}〉 ∈ {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))})) | 
| 113 | 111, 112 | sylibr 234 | . . 3
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}〉 ∈ (((𝑀 Sat 𝐸)‘∅) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))})) | 
| 114 |  | eqid 2736 | . . . . . 6
⊢ (𝑀 Sat 𝐸) = (𝑀 Sat 𝐸) | 
| 115 | 114 | satfv1 35369 | . . . . 5
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((𝑀 Sat 𝐸)‘1o) = (((𝑀 Sat 𝐸)‘∅) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))})) | 
| 116 | 115 | eleq2d 2826 | . . . 4
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}〉 ∈ ((𝑀 Sat 𝐸)‘1o) ↔ 〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}〉 ∈ (((𝑀 Sat 𝐸)‘∅) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))}))) | 
| 117 | 116 | 3ad2ant1 1133 | . . 3
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}〉 ∈ ((𝑀 Sat 𝐸)‘1o) ↔ 〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}〉 ∈ (((𝑀 Sat 𝐸)‘∅) ∪ {〈𝑥, 𝑦〉 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀𝑔𝑛(𝑖∈𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))}))) | 
| 118 | 113, 117 | mpbird 257 | . 2
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}〉 ∈ ((𝑀 Sat 𝐸)‘1o)) | 
| 119 |  | funopfv 6957 | . 2
⊢ (Fun
((𝑀 Sat 𝐸)‘1o) → (〈𝑋, {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}〉 ∈ ((𝑀 Sat 𝐸)‘1o) → (((𝑀 Sat 𝐸)‘1o)‘𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))})) | 
| 120 | 8, 118, 119 | sylc 65 | 1
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (((𝑀 Sat 𝐸)‘1o)‘𝑋) = {𝑎 ∈ (𝑀 ↑m ω) ∣ (¬
(𝑎‘𝐼)𝐸(𝑎‘𝐽) ∨ ¬ (𝑎‘𝐾)𝐸(𝑎‘𝐿))}) |