| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpll 767 | . . . . . 6
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝐼 ∈
ω) | 
| 2 |  | simplr 769 | . . . . . 6
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝐽 ∈
ω) | 
| 3 |  | simprl 771 | . . . . . 6
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝐾 ∈
ω) | 
| 4 |  | simprr 773 | . . . . . . . 8
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝐿 ∈
ω) | 
| 5 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑛 = 𝐿 → (𝐾∈𝑔𝑛) = (𝐾∈𝑔𝐿)) | 
| 6 | 5 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑛 = 𝐿 → ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑛)) = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿))) | 
| 7 | 6 | eqeq2d 2748 | . . . . . . . . 9
⊢ (𝑛 = 𝐿 → (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑛)) ↔ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿)))) | 
| 8 | 7 | adantl 481 | . . . . . . . 8
⊢ ((((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) ∧ 𝑛 = 𝐿) → (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑛)) ↔ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿)))) | 
| 9 |  | satfv1fvfmla1.x | . . . . . . . . 9
⊢ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿)) | 
| 10 | 9 | a1i 11 | . . . . . . . 8
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝐿))) | 
| 11 | 4, 8, 10 | rspcedvd 3624 | . . . . . . 7
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) →
∃𝑛 ∈ ω
𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑛))) | 
| 12 | 11 | orcd 874 | . . . . . 6
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) →
(∃𝑛 ∈ ω
𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑛)) ∨ 𝑋 = ∀𝑔𝐾(𝐼∈𝑔𝐽))) | 
| 13 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → (𝑖∈𝑔𝑗) = (𝐼∈𝑔𝑗)) | 
| 14 | 13 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝑖 = 𝐼 → ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛))) | 
| 15 | 14 | eqeq2d 2748 | . . . . . . . . 9
⊢ (𝑖 = 𝐼 → (𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ↔ 𝑋 = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)))) | 
| 16 | 15 | rexbidv 3179 | . . . . . . . 8
⊢ (𝑖 = 𝐼 → (∃𝑛 ∈ ω 𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ↔ ∃𝑛 ∈ ω 𝑋 = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)))) | 
| 17 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (𝑖 = 𝐼 → 𝑘 = 𝑘) | 
| 18 | 17, 13 | goaleq12d 35356 | . . . . . . . . 9
⊢ (𝑖 = 𝐼 → ∀𝑔𝑘(𝑖∈𝑔𝑗) = ∀𝑔𝑘(𝐼∈𝑔𝑗)) | 
| 19 | 18 | eqeq2d 2748 | . . . . . . . 8
⊢ (𝑖 = 𝐼 → (𝑋 = ∀𝑔𝑘(𝑖∈𝑔𝑗) ↔ 𝑋 = ∀𝑔𝑘(𝐼∈𝑔𝑗))) | 
| 20 | 16, 19 | orbi12d 919 | . . . . . . 7
⊢ (𝑖 = 𝐼 → ((∃𝑛 ∈ ω 𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑋 = ∀𝑔𝑘(𝑖∈𝑔𝑗)) ↔ (∃𝑛 ∈ ω 𝑋 = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑋 = ∀𝑔𝑘(𝐼∈𝑔𝑗)))) | 
| 21 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑗 = 𝐽 → (𝐼∈𝑔𝑗) = (𝐼∈𝑔𝐽)) | 
| 22 | 21 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝑗 = 𝐽 → ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑛))) | 
| 23 | 22 | eqeq2d 2748 | . . . . . . . . 9
⊢ (𝑗 = 𝐽 → (𝑋 = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ↔ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑛)))) | 
| 24 | 23 | rexbidv 3179 | . . . . . . . 8
⊢ (𝑗 = 𝐽 → (∃𝑛 ∈ ω 𝑋 = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ↔ ∃𝑛 ∈ ω 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑛)))) | 
| 25 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (𝑗 = 𝐽 → 𝑘 = 𝑘) | 
| 26 | 25, 21 | goaleq12d 35356 | . . . . . . . . 9
⊢ (𝑗 = 𝐽 → ∀𝑔𝑘(𝐼∈𝑔𝑗) = ∀𝑔𝑘(𝐼∈𝑔𝐽)) | 
| 27 | 26 | eqeq2d 2748 | . . . . . . . 8
⊢ (𝑗 = 𝐽 → (𝑋 = ∀𝑔𝑘(𝐼∈𝑔𝑗) ↔ 𝑋 = ∀𝑔𝑘(𝐼∈𝑔𝐽))) | 
| 28 | 24, 27 | orbi12d 919 | . . . . . . 7
⊢ (𝑗 = 𝐽 → ((∃𝑛 ∈ ω 𝑋 = ((𝐼∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑋 = ∀𝑔𝑘(𝐼∈𝑔𝑗)) ↔ (∃𝑛 ∈ ω 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑋 = ∀𝑔𝑘(𝐼∈𝑔𝐽)))) | 
| 29 |  | oveq1 7438 | . . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (𝑘∈𝑔𝑛) = (𝐾∈𝑔𝑛)) | 
| 30 | 29 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑛)) = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑛))) | 
| 31 | 30 | eqeq2d 2748 | . . . . . . . . 9
⊢ (𝑘 = 𝐾 → (𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑛)) ↔ 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑛)))) | 
| 32 | 31 | rexbidv 3179 | . . . . . . . 8
⊢ (𝑘 = 𝐾 → (∃𝑛 ∈ ω 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑛)) ↔ ∃𝑛 ∈ ω 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑛)))) | 
| 33 |  | id 22 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → 𝑘 = 𝐾) | 
| 34 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝐼∈𝑔𝐽) = (𝐼∈𝑔𝐽)) | 
| 35 | 33, 34 | goaleq12d 35356 | . . . . . . . . 9
⊢ (𝑘 = 𝐾 → ∀𝑔𝑘(𝐼∈𝑔𝐽) = ∀𝑔𝐾(𝐼∈𝑔𝐽)) | 
| 36 | 35 | eqeq2d 2748 | . . . . . . . 8
⊢ (𝑘 = 𝐾 → (𝑋 = ∀𝑔𝑘(𝐼∈𝑔𝐽) ↔ 𝑋 = ∀𝑔𝐾(𝐼∈𝑔𝐽))) | 
| 37 | 32, 36 | orbi12d 919 | . . . . . . 7
⊢ (𝑘 = 𝐾 → ((∃𝑛 ∈ ω 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑋 = ∀𝑔𝑘(𝐼∈𝑔𝐽)) ↔ (∃𝑛 ∈ ω 𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑛)) ∨ 𝑋 = ∀𝑔𝐾(𝐼∈𝑔𝐽)))) | 
| 38 | 20, 28, 37 | rspc3ev 3639 | . . . . . 6
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝐾 ∈ ω) ∧
(∃𝑛 ∈ ω
𝑋 = ((𝐼∈𝑔𝐽)⊼𝑔(𝐾∈𝑔𝑛)) ∨ 𝑋 = ∀𝑔𝐾(𝐼∈𝑔𝐽))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑛 ∈ ω 𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑋 = ∀𝑔𝑘(𝑖∈𝑔𝑗))) | 
| 39 | 1, 2, 3, 12, 38 | syl31anc 1375 | . . . . 5
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) →
∃𝑖 ∈ ω
∃𝑗 ∈ ω
∃𝑘 ∈ ω
(∃𝑛 ∈ ω
𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑋 = ∀𝑔𝑘(𝑖∈𝑔𝑗))) | 
| 40 | 9 | ovexi 7465 | . . . . . 6
⊢ 𝑋 ∈ V | 
| 41 |  | eqeq1 2741 | . . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ↔ 𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)))) | 
| 42 | 41 | rexbidv 3179 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (∃𝑛 ∈ ω 𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ↔ ∃𝑛 ∈ ω 𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)))) | 
| 43 |  | eqeq1 2741 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑥 = ∀𝑔𝑘(𝑖∈𝑔𝑗) ↔ 𝑋 = ∀𝑔𝑘(𝑖∈𝑔𝑗))) | 
| 44 | 42, 43 | orbi12d 919 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → ((∃𝑛 ∈ ω 𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑥 = ∀𝑔𝑘(𝑖∈𝑔𝑗)) ↔ (∃𝑛 ∈ ω 𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑋 = ∀𝑔𝑘(𝑖∈𝑔𝑗)))) | 
| 45 | 44 | rexbidv 3179 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (∃𝑘 ∈ ω (∃𝑛 ∈ ω 𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑥 = ∀𝑔𝑘(𝑖∈𝑔𝑗)) ↔ ∃𝑘 ∈ ω (∃𝑛 ∈ ω 𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑋 = ∀𝑔𝑘(𝑖∈𝑔𝑗)))) | 
| 46 | 45 | 2rexbidv 3222 | . . . . . 6
⊢ (𝑥 = 𝑋 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑛 ∈ ω 𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑥 = ∀𝑔𝑘(𝑖∈𝑔𝑗)) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑛 ∈ ω 𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑋 = ∀𝑔𝑘(𝑖∈𝑔𝑗)))) | 
| 47 | 40, 46 | elab 3679 | . . . . 5
⊢ (𝑋 ∈ {𝑥 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑛 ∈ ω 𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑥 = ∀𝑔𝑘(𝑖∈𝑔𝑗))} ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑛 ∈ ω 𝑋 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑋 = ∀𝑔𝑘(𝑖∈𝑔𝑗))) | 
| 48 | 39, 47 | sylibr 234 | . . . 4
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝑋 ∈ {𝑥 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑛 ∈ ω 𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑥 = ∀𝑔𝑘(𝑖∈𝑔𝑗))}) | 
| 49 | 48 | olcd 875 | . . 3
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (𝑋 ∈ ({∅} ×
(ω × ω)) ∨ 𝑋 ∈ {𝑥 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑛 ∈ ω 𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑥 = ∀𝑔𝑘(𝑖∈𝑔𝑗))})) | 
| 50 |  | elun 4153 | . . 3
⊢ (𝑋 ∈ (({∅} ×
(ω × ω)) ∪ {𝑥 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑛 ∈ ω 𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑥 = ∀𝑔𝑘(𝑖∈𝑔𝑗))}) ↔ (𝑋 ∈ ({∅} × (ω ×
ω)) ∨ 𝑋 ∈
{𝑥 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑛 ∈ ω 𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑥 = ∀𝑔𝑘(𝑖∈𝑔𝑗))})) | 
| 51 | 49, 50 | sylibr 234 | . 2
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝑋 ∈ (({∅} ×
(ω × ω)) ∪ {𝑥 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑘 ∈ ω (∃𝑛 ∈ ω 𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑥 = ∀𝑔𝑘(𝑖∈𝑔𝑗))})) | 
| 52 |  | fmla1 35392 | . 2
⊢
(Fmla‘1o) = (({∅} × (ω ×
ω)) ∪ {𝑥 ∣
∃𝑖 ∈ ω
∃𝑗 ∈ ω
∃𝑘 ∈ ω
(∃𝑛 ∈ ω
𝑥 = ((𝑖∈𝑔𝑗)⊼𝑔(𝑘∈𝑔𝑛)) ∨ 𝑥 = ∀𝑔𝑘(𝑖∈𝑔𝑗))}) | 
| 53 | 51, 52 | eleqtrrdi 2852 | 1
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝑋 ∈
(Fmla‘1o)) |