| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = ∅ →
(Fmla‘𝑥) =
(Fmla‘∅)) | 
| 2 | 1 | eleq2d 2826 | . . . . . 6
⊢ (𝑥 = ∅ → (𝐹 ∈ (Fmla‘𝑥) ↔ 𝐹 ∈
(Fmla‘∅))) | 
| 3 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = ∅ → ((∅ Sat
∅)‘𝑥) =
((∅ Sat ∅)‘∅)) | 
| 4 | 3 | eleq2d 2826 | . . . . . 6
⊢ (𝑥 = ∅ → (〈𝐹, ∅〉 ∈ ((∅
Sat ∅)‘𝑥)
↔ 〈𝐹,
∅〉 ∈ ((∅ Sat ∅)‘∅))) | 
| 5 | 2, 4 | bibi12d 345 | . . . . 5
⊢ (𝑥 = ∅ → ((𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥)) ↔
(𝐹 ∈
(Fmla‘∅) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘∅)))) | 
| 6 | 5 | imbi2d 340 | . . . 4
⊢ (𝑥 = ∅ → ((𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥))) ↔
(𝐹 ∈ V → (𝐹 ∈ (Fmla‘∅)
↔ 〈𝐹,
∅〉 ∈ ((∅ Sat ∅)‘∅))))) | 
| 7 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = 𝑦 → (Fmla‘𝑥) = (Fmla‘𝑦)) | 
| 8 | 7 | eleq2d 2826 | . . . . . 6
⊢ (𝑥 = 𝑦 → (𝐹 ∈ (Fmla‘𝑥) ↔ 𝐹 ∈ (Fmla‘𝑦))) | 
| 9 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat
∅)‘𝑦)) | 
| 10 | 9 | eleq2d 2826 | . . . . . 6
⊢ (𝑥 = 𝑦 → (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥) ↔
〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘𝑦))) | 
| 11 | 8, 10 | bibi12d 345 | . . . . 5
⊢ (𝑥 = 𝑦 → ((𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥)) ↔
(𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) | 
| 12 | 11 | imbi2d 340 | . . . 4
⊢ (𝑥 = 𝑦 → ((𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥))) ↔
(𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦))))) | 
| 13 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = suc 𝑦 → (Fmla‘𝑥) = (Fmla‘suc 𝑦)) | 
| 14 | 13 | eleq2d 2826 | . . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐹 ∈ (Fmla‘𝑥) ↔ 𝐹 ∈ (Fmla‘suc 𝑦))) | 
| 15 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = suc 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat
∅)‘suc 𝑦)) | 
| 16 | 15 | eleq2d 2826 | . . . . . 6
⊢ (𝑥 = suc 𝑦 → (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥) ↔
〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘suc 𝑦))) | 
| 17 | 14, 16 | bibi12d 345 | . . . . 5
⊢ (𝑥 = suc 𝑦 → ((𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥)) ↔
(𝐹 ∈ (Fmla‘suc
𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅
Sat ∅)‘suc 𝑦)))) | 
| 18 | 17 | imbi2d 340 | . . . 4
⊢ (𝑥 = suc 𝑦 → ((𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥))) ↔
(𝐹 ∈ V → (𝐹 ∈ (Fmla‘suc 𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘suc 𝑦))))) | 
| 19 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = 𝑁 → (Fmla‘𝑥) = (Fmla‘𝑁)) | 
| 20 | 19 | eleq2d 2826 | . . . . . 6
⊢ (𝑥 = 𝑁 → (𝐹 ∈ (Fmla‘𝑥) ↔ 𝐹 ∈ (Fmla‘𝑁))) | 
| 21 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = 𝑁 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat
∅)‘𝑁)) | 
| 22 | 21 | eleq2d 2826 | . . . . . 6
⊢ (𝑥 = 𝑁 → (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥) ↔
〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘𝑁))) | 
| 23 | 20, 22 | bibi12d 345 | . . . . 5
⊢ (𝑥 = 𝑁 → ((𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥)) ↔
(𝐹 ∈ (Fmla‘𝑁) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑁)))) | 
| 24 | 23 | imbi2d 340 | . . . 4
⊢ (𝑥 = 𝑁 → ((𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑥) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑥))) ↔
(𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑁) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑁))))) | 
| 25 |  | eqeq1 2740 | . . . . . . . 8
⊢ (𝑥 = 𝐹 → (𝑥 = (𝑖∈𝑔𝑗) ↔ 𝐹 = (𝑖∈𝑔𝑗))) | 
| 26 | 25 | 2rexbidv 3221 | . . . . . . 7
⊢ (𝑥 = 𝐹 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗))) | 
| 27 | 26 | elrab 3691 | . . . . . 6
⊢ (𝐹 ∈ {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} ↔ (𝐹 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗))) | 
| 28 |  | eqidd 2737 | . . . . . . . 8
⊢ ((𝐹 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)) → ∅ = ∅) | 
| 29 |  | simpr 484 | . . . . . . . 8
⊢ ((𝐹 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)) | 
| 30 | 28, 29 | jca 511 | . . . . . . 7
⊢ ((𝐹 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)) → (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝐹 = (𝑖∈𝑔𝑗))) | 
| 31 |  | simpr 484 | . . . . . . . . 9
⊢ ((∅
= ∅ ∧ ∃𝑖
∈ ω ∃𝑗
∈ ω 𝐹 = (𝑖∈𝑔𝑗)) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)) | 
| 32 | 31 | anim2i 617 | . . . . . . . 8
⊢ ((𝐹 ∈ V ∧ (∅ =
∅ ∧ ∃𝑖
∈ ω ∃𝑗
∈ ω 𝐹 = (𝑖∈𝑔𝑗))) → (𝐹 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗))) | 
| 33 | 32 | ex 412 | . . . . . . 7
⊢ (𝐹 ∈ V → ((∅ =
∅ ∧ ∃𝑖
∈ ω ∃𝑗
∈ ω 𝐹 = (𝑖∈𝑔𝑗)) → (𝐹 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)))) | 
| 34 | 30, 33 | impbid2 226 | . . . . . 6
⊢ (𝐹 ∈ V → ((𝐹 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)) ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝐹 = (𝑖∈𝑔𝑗)))) | 
| 35 | 27, 34 | bitrid 283 | . . . . 5
⊢ (𝐹 ∈ V → (𝐹 ∈ {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝐹 = (𝑖∈𝑔𝑗)))) | 
| 36 |  | fmla0 35388 | . . . . . . 7
⊢
(Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} | 
| 37 | 36 | eleq2i 2832 | . . . . . 6
⊢ (𝐹 ∈ (Fmla‘∅)
↔ 𝐹 ∈ {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)}) | 
| 38 | 37 | a1i 11 | . . . . 5
⊢ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘∅)
↔ 𝐹 ∈ {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)})) | 
| 39 |  | satf00 35380 | . . . . . . . 8
⊢ ((∅
Sat ∅)‘∅) = {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} | 
| 40 | 39 | a1i 11 | . . . . . . 7
⊢ (𝐹 ∈ V → ((∅ Sat
∅)‘∅) = {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))}) | 
| 41 | 40 | eleq2d 2826 | . . . . . 6
⊢ (𝐹 ∈ V → (〈𝐹, ∅〉 ∈ ((∅
Sat ∅)‘∅) ↔ 〈𝐹, ∅〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})) | 
| 42 |  | 0ex 5306 | . . . . . . 7
⊢ ∅
∈ V | 
| 43 |  | eqeq1 2740 | . . . . . . . . 9
⊢ (𝑦 = ∅ → (𝑦 = ∅ ↔ ∅ =
∅)) | 
| 44 | 43, 26 | bi2anan9r 639 | . . . . . . . 8
⊢ ((𝑥 = 𝐹 ∧ 𝑦 = ∅) → ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝐹 = (𝑖∈𝑔𝑗)))) | 
| 45 | 44 | opelopabga 5537 | . . . . . . 7
⊢ ((𝐹 ∈ V ∧ ∅ ∈
V) → (〈𝐹,
∅〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝐹 = (𝑖∈𝑔𝑗)))) | 
| 46 | 42, 45 | mpan2 691 | . . . . . 6
⊢ (𝐹 ∈ V → (〈𝐹, ∅〉 ∈
{〈𝑥, 𝑦〉 ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} ↔ (∅ = ∅ ∧
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝐹 = (𝑖∈𝑔𝑗)))) | 
| 47 | 41, 46 | bitrd 279 | . . . . 5
⊢ (𝐹 ∈ V → (〈𝐹, ∅〉 ∈ ((∅
Sat ∅)‘∅) ↔ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝐹 = (𝑖∈𝑔𝑗)))) | 
| 48 | 35, 38, 47 | 3bitr4d 311 | . . . 4
⊢ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘∅)
↔ 〈𝐹,
∅〉 ∈ ((∅ Sat ∅)‘∅))) | 
| 49 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ ∅ =
∅ | 
| 50 | 49 | biantrur 530 | . . . . . . . . . . 11
⊢
(∃𝑢 ∈
((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢)) ↔ (∅ = ∅ ∧
∃𝑢 ∈ ((∅
Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢)))) | 
| 51 | 50 | bicomi 224 | . . . . . . . . . 10
⊢ ((∅
= ∅ ∧ ∃𝑢
∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢))) ↔ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢))) | 
| 52 | 51 | a1i 11 | . . . . . . . . 9
⊢ (𝐹 ∈ V → ((∅ =
∅ ∧ ∃𝑢
∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢))) ↔ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢)))) | 
| 53 |  | eqeq1 2740 | . . . . . . . . . . . 12
⊢ (𝑧 = ∅ → (𝑧 = ∅ ↔ ∅ =
∅)) | 
| 54 |  | eqeq1 2740 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐹 → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔ 𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) | 
| 55 | 54 | rexbidv 3178 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐹 → (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔
∃𝑣 ∈ ((∅
Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) | 
| 56 |  | eqeq1 2740 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐹 → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ 𝐹 = ∀𝑔𝑖(1st ‘𝑢))) | 
| 57 | 56 | rexbidv 3178 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐹 → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝐹 =
∀𝑔𝑖(1st ‘𝑢))) | 
| 58 | 55, 57 | orbi12d 918 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝐹 → ((∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢)))) | 
| 59 | 58 | rexbidv 3178 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝐹 → (∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ↔ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢)))) | 
| 60 | 53, 59 | bi2anan9r 639 | . . . . . . . . . . 11
⊢ ((𝑥 = 𝐹 ∧ 𝑧 = ∅) → ((𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) ↔ (∅ = ∅ ∧
∃𝑢 ∈ ((∅
Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢))))) | 
| 61 | 60 | opelopabga 5537 | . . . . . . . . . 10
⊢ ((𝐹 ∈ V ∧ ∅ ∈
V) → (〈𝐹,
∅〉 ∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} ↔ (∅ = ∅ ∧
∃𝑢 ∈ ((∅
Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢))))) | 
| 62 | 42, 61 | mpan2 691 | . . . . . . . . 9
⊢ (𝐹 ∈ V → (〈𝐹, ∅〉 ∈
{〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} ↔ (∅ = ∅ ∧
∃𝑢 ∈ ((∅
Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢))))) | 
| 63 | 59 | elabg 3675 | . . . . . . . . 9
⊢ (𝐹 ∈ V → (𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))} ↔ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝐹 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝐹 =
∀𝑔𝑖(1st ‘𝑢)))) | 
| 64 | 52, 62, 63 | 3bitr4d 311 | . . . . . . . 8
⊢ (𝐹 ∈ V → (〈𝐹, ∅〉 ∈
{〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} ↔ 𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))})) | 
| 65 | 64 | adantl 481 | . . . . . . 7
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) →
(〈𝐹, ∅〉
∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} ↔ 𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))})) | 
| 66 | 65 | orbi2d 915 | . . . . . 6
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) →
((〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘𝑦) ∨ 〈𝐹, ∅〉 ∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦) ∨
𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}))) | 
| 67 |  | eqid 2736 | . . . . . . . . . 10
⊢ (∅
Sat ∅) = (∅ Sat ∅) | 
| 68 | 67 | satf0suc 35382 | . . . . . . . . 9
⊢ (𝑦 ∈ ω → ((∅
Sat ∅)‘suc 𝑦) =
(((∅ Sat ∅)‘𝑦) ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) | 
| 69 | 68 | eleq2d 2826 | . . . . . . . 8
⊢ (𝑦 ∈ ω →
(〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘suc 𝑦) ↔ 〈𝐹, ∅〉 ∈ (((∅ Sat
∅)‘𝑦) ∪
{〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))) | 
| 70 |  | elun 4152 | . . . . . . . 8
⊢
(〈𝐹,
∅〉 ∈ (((∅ Sat ∅)‘𝑦) ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦) ∨
〈𝐹, ∅〉
∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) | 
| 71 | 69, 70 | bitrdi 287 | . . . . . . 7
⊢ (𝑦 ∈ ω →
(〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘suc 𝑦) ↔ (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦) ∨
〈𝐹, ∅〉
∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))) | 
| 72 | 71 | ad2antrr 726 | . . . . . 6
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) →
(〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘suc 𝑦) ↔ (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦) ∨
〈𝐹, ∅〉
∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))) | 
| 73 |  | fmlasuc0 35390 | . . . . . . . . 9
⊢ (𝑦 ∈ ω →
(Fmla‘suc 𝑦) =
((Fmla‘𝑦) ∪
{𝑥 ∣ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))})) | 
| 74 | 73 | eleq2d 2826 | . . . . . . . 8
⊢ (𝑦 ∈ ω → (𝐹 ∈ (Fmla‘suc 𝑦) ↔ 𝐹 ∈ ((Fmla‘𝑦) ∪ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}))) | 
| 75 | 74 | ad2antrr 726 | . . . . . . 7
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) → (𝐹 ∈ (Fmla‘suc 𝑦) ↔ 𝐹 ∈ ((Fmla‘𝑦) ∪ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}))) | 
| 76 |  | elun 4152 | . . . . . . . 8
⊢ (𝐹 ∈ ((Fmla‘𝑦) ∪ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}) ↔ (𝐹 ∈ (Fmla‘𝑦) ∨ 𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))})) | 
| 77 | 76 | a1i 11 | . . . . . . 7
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) → (𝐹 ∈ ((Fmla‘𝑦) ∪ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}) ↔ (𝐹 ∈ (Fmla‘𝑦) ∨ 𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}))) | 
| 78 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) →
(𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) | 
| 79 | 78 | imp 406 | . . . . . . . 8
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦))) | 
| 80 | 79 | orbi1d 916 | . . . . . . 7
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) → ((𝐹 ∈ (Fmla‘𝑦) ∨ 𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}) ↔ (〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦) ∨
𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}))) | 
| 81 | 75, 77, 80 | 3bitrd 305 | . . . . . 6
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) → (𝐹 ∈ (Fmla‘suc 𝑦) ↔ (〈𝐹, ∅〉 ∈ ((∅
Sat ∅)‘𝑦) ∨
𝐹 ∈ {𝑥 ∣ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))}))) | 
| 82 | 66, 72, 81 | 3bitr4rd 312 | . . . . 5
⊢ (((𝑦 ∈ ω ∧ (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦)))) ∧
𝐹 ∈ V) → (𝐹 ∈ (Fmla‘suc 𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘suc 𝑦))) | 
| 83 | 82 | exp31 419 | . . . 4
⊢ (𝑦 ∈ ω → ((𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑦))) →
(𝐹 ∈ V → (𝐹 ∈ (Fmla‘suc 𝑦) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘suc 𝑦))))) | 
| 84 | 6, 12, 18, 24, 48, 83 | finds 7919 | . . 3
⊢ (𝑁 ∈ ω → (𝐹 ∈ V → (𝐹 ∈ (Fmla‘𝑁) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑁)))) | 
| 85 | 84 | com12 32 | . 2
⊢ (𝐹 ∈ V → (𝑁 ∈ ω → (𝐹 ∈ (Fmla‘𝑁) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑁)))) | 
| 86 |  | prcnel 3506 | . . . . 5
⊢ (¬
𝐹 ∈ V → ¬
𝐹 ∈ (Fmla‘𝑁)) | 
| 87 | 86 | adantr 480 | . . . 4
⊢ ((¬
𝐹 ∈ V ∧ 𝑁 ∈ ω) → ¬
𝐹 ∈ (Fmla‘𝑁)) | 
| 88 |  | opprc1 4896 | . . . . . 6
⊢ (¬
𝐹 ∈ V →
〈𝐹, ∅〉 =
∅) | 
| 89 | 88 | adantr 480 | . . . . 5
⊢ ((¬
𝐹 ∈ V ∧ 𝑁 ∈ ω) →
〈𝐹, ∅〉 =
∅) | 
| 90 |  | satf0n0 35384 | . . . . . . 7
⊢ (𝑁 ∈ ω → ∅
∉ ((∅ Sat ∅)‘𝑁)) | 
| 91 |  | df-nel 3046 | . . . . . . 7
⊢ (∅
∉ ((∅ Sat ∅)‘𝑁) ↔ ¬ ∅ ∈ ((∅ Sat
∅)‘𝑁)) | 
| 92 | 90, 91 | sylib 218 | . . . . . 6
⊢ (𝑁 ∈ ω → ¬
∅ ∈ ((∅ Sat ∅)‘𝑁)) | 
| 93 | 92 | adantl 481 | . . . . 5
⊢ ((¬
𝐹 ∈ V ∧ 𝑁 ∈ ω) → ¬
∅ ∈ ((∅ Sat ∅)‘𝑁)) | 
| 94 | 89, 93 | eqneltrd 2860 | . . . 4
⊢ ((¬
𝐹 ∈ V ∧ 𝑁 ∈ ω) → ¬
〈𝐹, ∅〉
∈ ((∅ Sat ∅)‘𝑁)) | 
| 95 | 87, 94 | 2falsed 376 | . . 3
⊢ ((¬
𝐹 ∈ V ∧ 𝑁 ∈ ω) → (𝐹 ∈ (Fmla‘𝑁) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑁))) | 
| 96 | 95 | ex 412 | . 2
⊢ (¬
𝐹 ∈ V → (𝑁 ∈ ω → (𝐹 ∈ (Fmla‘𝑁) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑁)))) | 
| 97 | 85, 96 | pm2.61i 182 | 1
⊢ (𝑁 ∈ ω → (𝐹 ∈ (Fmla‘𝑁) ↔ 〈𝐹, ∅〉 ∈ ((∅ Sat
∅)‘𝑁))) |