| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6905 | . . 3
⊢ (𝑥 = ∅ → ((∅ Sat
∅)‘𝑥) =
((∅ Sat ∅)‘∅)) | 
| 2 | 1 | raleqdv 3325 | . 2
⊢ (𝑥 = ∅ → (∀𝑤 ∈ ((∅ Sat
∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat
∅)‘∅)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))) | 
| 3 |  | fveq2 6905 | . . 3
⊢ (𝑥 = 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat
∅)‘𝑦)) | 
| 4 | 3 | raleqdv 3325 | . 2
⊢ (𝑥 = 𝑦 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))) | 
| 5 |  | fveq2 6905 | . . 3
⊢ (𝑥 = suc 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat
∅)‘suc 𝑦)) | 
| 6 | 5 | raleqdv 3325 | . 2
⊢ (𝑥 = suc 𝑦 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘suc
𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))) | 
| 7 |  | fveq2 6905 | . . 3
⊢ (𝑥 = 𝑁 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat
∅)‘𝑁)) | 
| 8 | 7 | raleqdv 3325 | . 2
⊢ (𝑥 = 𝑁 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑁)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))) | 
| 9 |  | eqeq1 2740 | . . . . . . . 8
⊢ (𝑥 = (1st ‘𝑤) → (𝑥 = (𝑖∈𝑔𝑗) ↔ (1st ‘𝑤) = (𝑖∈𝑔𝑗))) | 
| 10 | 9 | 2rexbidv 3221 | . . . . . . 7
⊢ (𝑥 = (1st ‘𝑤) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗))) | 
| 11 | 10 | anbi2d 630 | . . . . . 6
⊢ (𝑥 = (1st ‘𝑤) → ((𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) ↔ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)))) | 
| 12 |  | eqeq1 2740 | . . . . . . 7
⊢ (𝑧 = (2nd ‘𝑤) → (𝑧 = ∅ ↔ (2nd
‘𝑤) =
∅)) | 
| 13 | 12 | anbi1d 631 | . . . . . 6
⊢ (𝑧 = (2nd ‘𝑤) → ((𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)) ↔ ((2nd ‘𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st
‘𝑤) = (𝑖∈𝑔𝑗)))) | 
| 14 | 11, 13 | elopabi 8088 | . . . . 5
⊢ (𝑤 ∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} → ((2nd ‘𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st
‘𝑤) = (𝑖∈𝑔𝑗))) | 
| 15 |  | goel 35353 | . . . . . . . . 9
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖∈𝑔𝑗) = 〈∅, 〈𝑖, 𝑗〉〉) | 
| 16 | 15 | eqeq2d 2747 | . . . . . . . 8
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) →
((1st ‘𝑤)
= (𝑖∈𝑔𝑗) ↔ (1st ‘𝑤) = 〈∅, 〈𝑖, 𝑗〉〉)) | 
| 17 |  | omex 9684 | . . . . . . . . . . 11
⊢ ω
∈ V | 
| 18 | 17, 17 | pm3.2i 470 | . . . . . . . . . 10
⊢ (ω
∈ V ∧ ω ∈ V) | 
| 19 |  | peano1 7911 | . . . . . . . . . . . 12
⊢ ∅
∈ ω | 
| 20 | 19 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ∅
∈ ω) | 
| 21 |  | opelxpi 5721 | . . . . . . . . . . 11
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) →
〈𝑖, 𝑗〉 ∈ (ω ×
ω)) | 
| 22 | 20, 21 | opelxpd 5723 | . . . . . . . . . 10
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) →
〈∅, 〈𝑖,
𝑗〉〉 ∈
(ω × (ω × ω))) | 
| 23 |  | xpeq12 5709 | . . . . . . . . . . . . 13
⊢ ((𝑎 = ω ∧ 𝑏 = ω) → (𝑎 × 𝑏) = (ω ×
ω)) | 
| 24 | 23 | xpeq2d 5714 | . . . . . . . . . . . 12
⊢ ((𝑎 = ω ∧ 𝑏 = ω) → (ω
× (𝑎 × 𝑏)) = (ω × (ω
× ω))) | 
| 25 | 24 | eleq2d 2826 | . . . . . . . . . . 11
⊢ ((𝑎 = ω ∧ 𝑏 = ω) →
(〈∅, 〈𝑖,
𝑗〉〉 ∈
(ω × (𝑎 ×
𝑏)) ↔ 〈∅,
〈𝑖, 𝑗〉〉 ∈ (ω × (ω
× ω)))) | 
| 26 | 25 | spc2egv 3598 | . . . . . . . . . 10
⊢ ((ω
∈ V ∧ ω ∈ V) → (〈∅, 〈𝑖, 𝑗〉〉 ∈ (ω × (ω
× ω)) → ∃𝑎∃𝑏〈∅, 〈𝑖, 𝑗〉〉 ∈ (ω × (𝑎 × 𝑏)))) | 
| 27 | 18, 22, 26 | mpsyl 68 | . . . . . . . . 9
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) →
∃𝑎∃𝑏〈∅, 〈𝑖, 𝑗〉〉 ∈ (ω × (𝑎 × 𝑏))) | 
| 28 |  | eleq1 2828 | . . . . . . . . . 10
⊢
((1st ‘𝑤) = 〈∅, 〈𝑖, 𝑗〉〉 → ((1st
‘𝑤) ∈ (ω
× (𝑎 × 𝑏)) ↔ 〈∅,
〈𝑖, 𝑗〉〉 ∈ (ω × (𝑎 × 𝑏)))) | 
| 29 | 28 | 2exbidv 1923 | . . . . . . . . 9
⊢
((1st ‘𝑤) = 〈∅, 〈𝑖, 𝑗〉〉 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏〈∅, 〈𝑖, 𝑗〉〉 ∈ (ω × (𝑎 × 𝑏)))) | 
| 30 | 27, 29 | syl5ibrcom 247 | . . . . . . . 8
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) →
((1st ‘𝑤)
= 〈∅, 〈𝑖,
𝑗〉〉 →
∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))) | 
| 31 | 16, 30 | sylbid 240 | . . . . . . 7
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) →
((1st ‘𝑤)
= (𝑖∈𝑔𝑗) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))) | 
| 32 | 31 | rexlimivv 3200 | . . . . . 6
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω (1st ‘𝑤) = (𝑖∈𝑔𝑗) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) | 
| 33 | 32 | adantl 481 | . . . . 5
⊢
(((2nd ‘𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) | 
| 34 | 14, 33 | syl 17 | . . . 4
⊢ (𝑤 ∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) | 
| 35 |  | satf00 35380 | . . . 4
⊢ ((∅
Sat ∅)‘∅) = {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} | 
| 36 | 34, 35 | eleq2s 2858 | . . 3
⊢ (𝑤 ∈ ((∅ Sat
∅)‘∅) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) | 
| 37 | 36 | rgen 3062 | . 2
⊢
∀𝑤 ∈
((∅ Sat ∅)‘∅)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) | 
| 38 |  | omsucelsucb 8499 | . . . . . . . . . . 11
⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈ suc
ω) | 
| 39 |  | satf0sucom 35379 | . . . . . . . . . . 11
⊢ (suc
𝑦 ∈ suc ω →
((∅ Sat ∅)‘suc 𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑦)) | 
| 40 | 38, 39 | sylbi 217 | . . . . . . . . . 10
⊢ (𝑦 ∈ ω → ((∅
Sat ∅)‘suc 𝑦) =
(rec((𝑓 ∈ V ↦
(𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑦)) | 
| 41 | 40 | adantr 480 | . . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((∅ Sat ∅)‘suc
𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑦)) | 
| 42 |  | nnon 7894 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ω → 𝑦 ∈ On) | 
| 43 |  | rdgsuc 8465 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ On → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑦) = ((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦))) | 
| 44 | 42, 43 | syl 17 | . . . . . . . . . . 11
⊢ (𝑦 ∈ ω →
(rec((𝑓 ∈ V ↦
(𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑦) = ((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦))) | 
| 45 | 44 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑦) = ((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦))) | 
| 46 |  | elelsuc 6456 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ω → 𝑦 ∈ suc
ω) | 
| 47 |  | satf0sucom 35379 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ suc ω →
((∅ Sat ∅)‘𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦)) | 
| 48 | 46, 47 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ω → ((∅
Sat ∅)‘𝑦) =
(rec((𝑓 ∈ V ↦
(𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦)) | 
| 49 | 48 | eqcomd 2742 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ω →
(rec((𝑓 ∈ V ↦
(𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦) = ((∅ Sat ∅)‘𝑦)) | 
| 50 | 49 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝑦 ∈ ω → ((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦)) = ((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘((∅ Sat
∅)‘𝑦))) | 
| 51 | 50 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦)) = ((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘((∅ Sat
∅)‘𝑦))) | 
| 52 |  | eqidd 2737 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) = (𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))) | 
| 53 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝑓 = ((∅ Sat
∅)‘𝑦) →
𝑓 = ((∅ Sat
∅)‘𝑦)) | 
| 54 |  | rexeq 3321 | . . . . . . . . . . . . . . . . 17
⊢ (𝑓 = ((∅ Sat
∅)‘𝑦) →
(∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔
∃𝑣 ∈ ((∅
Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) | 
| 55 | 54 | orbi1d 916 | . . . . . . . . . . . . . . . 16
⊢ (𝑓 = ((∅ Sat
∅)‘𝑦) →
((∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) | 
| 56 | 55 | rexeqbi1dv 3338 | . . . . . . . . . . . . . . 15
⊢ (𝑓 = ((∅ Sat
∅)‘𝑦) →
(∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ↔ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) | 
| 57 | 56 | anbi2d 630 | . . . . . . . . . . . . . 14
⊢ (𝑓 = ((∅ Sat
∅)‘𝑦) →
((𝑧 = ∅ ∧
∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) ↔ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) | 
| 58 | 57 | opabbidv 5208 | . . . . . . . . . . . . 13
⊢ (𝑓 = ((∅ Sat
∅)‘𝑦) →
{〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} = {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) | 
| 59 | 53, 58 | uneq12d 4168 | . . . . . . . . . . . 12
⊢ (𝑓 = ((∅ Sat
∅)‘𝑦) →
(𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) = (((∅ Sat ∅)‘𝑦) ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) | 
| 60 | 59 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) ∧ 𝑓 = ((∅ Sat ∅)‘𝑦)) → (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) = (((∅ Sat ∅)‘𝑦) ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) | 
| 61 |  | fvexd 6920 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((∅ Sat ∅)‘𝑦) ∈ V) | 
| 62 | 17 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ω ∈ V) | 
| 63 |  | satf0suclem 35381 | . . . . . . . . . . . . 13
⊢
((((∅ Sat ∅)‘𝑦) ∈ V ∧ ((∅ Sat
∅)‘𝑦) ∈ V
∧ ω ∈ V) → {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} ∈ V) | 
| 64 | 61, 61, 62, 63 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} ∈ V) | 
| 65 |  | unexg 7764 | . . . . . . . . . . . 12
⊢
((((∅ Sat ∅)‘𝑦) ∈ V ∧ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} ∈ V) → (((∅ Sat
∅)‘𝑦) ∪
{〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) ∈ V) | 
| 66 | 61, 64, 65 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (((∅ Sat
∅)‘𝑦) ∪
{〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) ∈ V) | 
| 67 | 52, 60, 61, 66 | fvmptd 7022 | . . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))‘((∅ Sat
∅)‘𝑦)) =
(((∅ Sat ∅)‘𝑦) ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) | 
| 68 | 45, 51, 67 | 3eqtrd 2780 | . . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})), {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑦) = (((∅ Sat ∅)‘𝑦) ∪ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) | 
| 69 | 41, 68 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((∅ Sat ∅)‘suc
𝑦) = (((∅ Sat
∅)‘𝑦) ∪
{〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) | 
| 70 | 69 | eleq2d 2826 | . . . . . . 7
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘suc
𝑦) ↔ 𝑡 ∈ (((∅ Sat
∅)‘𝑦) ∪
{〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))) | 
| 71 |  | elun 4152 | . . . . . . 7
⊢ (𝑡 ∈ (((∅ Sat
∅)‘𝑦) ∪
{〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) ↔ (𝑡 ∈ ((∅ Sat ∅)‘𝑦) ∨ 𝑡 ∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))})) | 
| 72 | 70, 71 | bitrdi 287 | . . . . . 6
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘suc
𝑦) ↔ (𝑡 ∈ ((∅ Sat
∅)‘𝑦) ∨
𝑡 ∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}))) | 
| 73 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑡 → (1st ‘𝑤) = (1st ‘𝑡)) | 
| 74 | 73 | eleq1d 2825 | . . . . . . . . . 10
⊢ (𝑤 = 𝑡 → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))) | 
| 75 | 74 | 2exbidv 1923 | . . . . . . . . 9
⊢ (𝑤 = 𝑡 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))) | 
| 76 | 75 | rspccv 3618 | . . . . . . . 8
⊢
(∀𝑤 ∈
((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑡 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))) | 
| 77 | 76 | adantl 481 | . . . . . . 7
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))) | 
| 78 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑣 → (1st ‘𝑤) = (1st ‘𝑣)) | 
| 79 | 78 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑣 → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏)))) | 
| 80 | 79 | 2exbidv 1923 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑣 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏(1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏)))) | 
| 81 | 80 | rspcva 3619 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ ((∅ Sat
∅)‘𝑦) ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏))) | 
| 82 |  | sels 5442 | . . . . . . . . . . . . . . . . . 18
⊢
((1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑣) ∈ 𝑠) | 
| 83 | 82 | exlimivv 1931 | . . . . . . . . . . . . . . . . 17
⊢
(∃𝑎∃𝑏(1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑣) ∈ 𝑠) | 
| 84 | 81, 83 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ ((∅ Sat
∅)‘𝑦) ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑠(1st ‘𝑣) ∈ 𝑠) | 
| 85 | 84 | expcom 413 | . . . . . . . . . . . . . . 15
⊢
(∀𝑤 ∈
((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑣 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑠(1st ‘𝑣) ∈ 𝑠)) | 
| 86 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑢 → (1st ‘𝑤) = (1st ‘𝑢)) | 
| 87 | 86 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑢 → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)))) | 
| 88 | 87 | 2exbidv 1923 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑢 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏(1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)))) | 
| 89 | 88 | rspcva 3619 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ ((∅ Sat
∅)‘𝑦) ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏))) | 
| 90 |  | sels 5442 | . . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑢) ∈ 𝑠) | 
| 91 | 90 | exlimivv 1931 | . . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑎∃𝑏(1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑢) ∈ 𝑠) | 
| 92 | 89, 91 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ ((∅ Sat
∅)‘𝑦) ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑠(1st ‘𝑢) ∈ 𝑠) | 
| 93 |  | eleq2w 2824 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = 𝑟 → ((1st ‘𝑢) ∈ 𝑠 ↔ (1st ‘𝑢) ∈ 𝑟)) | 
| 94 | 93 | cbvexvw 2035 | . . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑠(1st ‘𝑢) ∈ 𝑠 ↔ ∃𝑟(1st ‘𝑢) ∈ 𝑟) | 
| 95 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑟 ∈ V | 
| 96 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑠 ∈ V | 
| 97 | 95, 96 | pm3.2i 470 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑟 ∈ V ∧ 𝑠 ∈ V) | 
| 98 |  | df-ov 7435 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) =
(⊼𝑔‘〈(1st ‘𝑢), (1st ‘𝑣)〉) | 
| 99 |  | df-gona 35347 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
⊼𝑔 = (𝑒 ∈ (V × V) ↦
〈1o, 𝑒〉) | 
| 100 |  | opeq2 4873 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑒 = 〈(1st
‘𝑢), (1st
‘𝑣)〉 →
〈1o, 𝑒〉 = 〈1o,
〈(1st ‘𝑢), (1st ‘𝑣)〉〉) | 
| 101 |  | opelvvg 5725 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → 〈(1st ‘𝑢), (1st ‘𝑣)〉 ∈ (V ×
V)) | 
| 102 |  | opex 5468 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
〈1o, 〈(1st ‘𝑢), (1st ‘𝑣)〉〉 ∈ V | 
| 103 | 102 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → 〈1o,
〈(1st ‘𝑢), (1st ‘𝑣)〉〉 ∈ V) | 
| 104 | 99, 100, 101, 103 | fvmptd3 7038 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) →
(⊼𝑔‘〈(1st ‘𝑢), (1st ‘𝑣)〉) = 〈1o,
〈(1st ‘𝑢), (1st ‘𝑣)〉〉) | 
| 105 | 98, 104 | eqtrid 2788 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) =
〈1o, 〈(1st ‘𝑢), (1st ‘𝑣)〉〉) | 
| 106 |  | 1onn 8679 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
1o ∈ ω | 
| 107 | 106 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → 1o ∈
ω) | 
| 108 |  | opelxpi 5721 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → 〈(1st ‘𝑢), (1st ‘𝑣)〉 ∈ (𝑟 × 𝑠)) | 
| 109 | 107, 108 | opelxpd 5723 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → 〈1o,
〈(1st ‘𝑢), (1st ‘𝑣)〉〉 ∈ (ω × (𝑟 × 𝑠))) | 
| 110 | 105, 109 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∈ (ω
× (𝑟 × 𝑠))) | 
| 111 |  | xpeq12 5709 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑎 = 𝑟 ∧ 𝑏 = 𝑠) → (𝑎 × 𝑏) = (𝑟 × 𝑠)) | 
| 112 | 111 | xpeq2d 5714 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 = 𝑟 ∧ 𝑏 = 𝑠) → (ω × (𝑎 × 𝑏)) = (ω × (𝑟 × 𝑠))) | 
| 113 | 112 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 = 𝑟 ∧ 𝑏 = 𝑠) → (((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∈ (ω
× (𝑎 × 𝑏)) ↔ ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) ∈ (ω
× (𝑟 × 𝑠)))) | 
| 114 | 113 | spc2egv 3598 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑟 ∈ V ∧ 𝑠 ∈ V) →
(((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∈ (ω
× (𝑟 × 𝑠)) → ∃𝑎∃𝑏((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∈ (ω
× (𝑎 × 𝑏)))) | 
| 115 | 97, 110, 114 | mpsyl 68 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ∃𝑎∃𝑏((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∈ (ω
× (𝑎 × 𝑏))) | 
| 116 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) →
((1st ‘𝑡)
∈ (ω × (𝑎
× 𝑏)) ↔
((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∈ (ω
× (𝑎 × 𝑏)))) | 
| 117 | 116 | 2exbidv 1923 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) →
(∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∈ (ω
× (𝑎 × 𝑏)))) | 
| 118 | 115, 117 | syl5ibrcom 247 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ((1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) →
∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))) | 
| 119 | 118 | ex 412 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((1st ‘𝑢) ∈ 𝑟 → ((1st ‘𝑣) ∈ 𝑠 → ((1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) →
∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))) | 
| 120 | 119 | exlimdv 1932 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((1st ‘𝑢) ∈ 𝑟 → (∃𝑠(1st ‘𝑣) ∈ 𝑠 → ((1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) →
∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))) | 
| 121 | 120 | com23 86 | . . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑢) ∈ 𝑟 → ((1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) →
(∃𝑠(1st
‘𝑣) ∈ 𝑠 → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))) | 
| 122 | 121 | exlimiv 1929 | . . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑟(1st ‘𝑢) ∈ 𝑟 → ((1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) →
(∃𝑠(1st
‘𝑣) ∈ 𝑠 → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))) | 
| 123 | 94, 122 | sylbi 217 | . . . . . . . . . . . . . . . . . 18
⊢
(∃𝑠(1st ‘𝑢) ∈ 𝑠 → ((1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) →
(∃𝑠(1st
‘𝑣) ∈ 𝑠 → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))) | 
| 124 | 92, 123 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ((∅ Sat
∅)‘𝑦) ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) →
(∃𝑠(1st
‘𝑣) ∈ 𝑠 → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))) | 
| 125 | 124 | expcom 413 | . . . . . . . . . . . . . . . 16
⊢
(∀𝑤 ∈
((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → ((1st
‘𝑡) =
((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) →
(∃𝑠(1st
‘𝑣) ∈ 𝑠 → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))) | 
| 126 | 125 | com24 95 | . . . . . . . . . . . . . . 15
⊢
(∀𝑤 ∈
((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → (∃𝑠(1st ‘𝑣) ∈ 𝑠 → ((1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) → (𝑢 ∈ ((∅ Sat
∅)‘𝑦) →
∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))) | 
| 127 | 85, 126 | syld 47 | . . . . . . . . . . . . . 14
⊢
(∀𝑤 ∈
((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑣 ∈ ((∅ Sat ∅)‘𝑦) → ((1st
‘𝑡) =
((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) → (𝑢 ∈ ((∅ Sat
∅)‘𝑦) →
∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))) | 
| 128 | 127 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑣 ∈ ((∅ Sat ∅)‘𝑦) → ((1st
‘𝑡) =
((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) → (𝑢 ∈ ((∅ Sat
∅)‘𝑦) →
∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))) | 
| 129 | 128 | com14 96 | . . . . . . . . . . . 12
⊢ (𝑢 ∈ ((∅ Sat
∅)‘𝑦) →
(𝑣 ∈ ((∅ Sat
∅)‘𝑦) →
((1st ‘𝑡)
= ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) → ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))) | 
| 130 | 129 | rexlimdv 3152 | . . . . . . . . . . 11
⊢ (𝑢 ∈ ((∅ Sat
∅)‘𝑦) →
(∃𝑣 ∈ ((∅
Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) → ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))) | 
| 131 | 17, 96 | pm3.2i 470 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (ω
∈ V ∧ 𝑠 ∈
V) | 
| 132 |  | df-goal 35348 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
∀𝑔𝑖(1st ‘𝑢) = 〈2o, 〈𝑖, (1st ‘𝑢)〉〉 | 
| 133 |  | 2onn 8681 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
2o ∈ ω | 
| 134 | 133 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → 2o ∈
ω) | 
| 135 |  | opelxpi 5721 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑖 ∈ ω ∧
(1st ‘𝑢)
∈ 𝑠) →
〈𝑖, (1st
‘𝑢)〉 ∈
(ω × 𝑠)) | 
| 136 | 135 | ancoms 458 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → 〈𝑖, (1st ‘𝑢)〉 ∈ (ω ×
𝑠)) | 
| 137 | 134, 136 | opelxpd 5723 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → 〈2o,
〈𝑖, (1st
‘𝑢)〉〉
∈ (ω × (ω × 𝑠))) | 
| 138 | 132, 137 | eqeltrid 2844 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) →
∀𝑔𝑖(1st ‘𝑢) ∈ (ω × (ω ×
𝑠))) | 
| 139 | 138 | 3adant3 1132 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω ∧ (1st
‘𝑡) =
∀𝑔𝑖(1st ‘𝑢)) → ∀𝑔𝑖(1st ‘𝑢) ∈ (ω ×
(ω × 𝑠))) | 
| 140 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢) → ((1st
‘𝑡) ∈ (ω
× (ω × 𝑠)) ↔ ∀𝑔𝑖(1st ‘𝑢) ∈ (ω ×
(ω × 𝑠)))) | 
| 141 | 140 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω ∧ (1st
‘𝑡) =
∀𝑔𝑖(1st ‘𝑢)) → ((1st ‘𝑡) ∈ (ω ×
(ω × 𝑠)) ↔
∀𝑔𝑖(1st ‘𝑢) ∈ (ω × (ω ×
𝑠)))) | 
| 142 | 139, 141 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω ∧ (1st
‘𝑡) =
∀𝑔𝑖(1st ‘𝑢)) → (1st ‘𝑡) ∈ (ω ×
(ω × 𝑠))) | 
| 143 |  | xpeq12 5709 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 = ω ∧ 𝑏 = 𝑠) → (𝑎 × 𝑏) = (ω × 𝑠)) | 
| 144 | 143 | xpeq2d 5714 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 = ω ∧ 𝑏 = 𝑠) → (ω × (𝑎 × 𝑏)) = (ω × (ω × 𝑠))) | 
| 145 | 144 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 = ω ∧ 𝑏 = 𝑠) → ((1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑡) ∈ (ω ×
(ω × 𝑠)))) | 
| 146 | 145 | spc2egv 3598 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((ω
∈ V ∧ 𝑠 ∈ V)
→ ((1st ‘𝑡) ∈ (ω × (ω ×
𝑠)) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))) | 
| 147 | 131, 142,
146 | mpsyl 68 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω ∧ (1st
‘𝑡) =
∀𝑔𝑖(1st ‘𝑢)) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))) | 
| 148 | 147 | 3exp 1119 | . . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑢) ∈ 𝑠 → (𝑖 ∈ ω → ((1st
‘𝑡) =
∀𝑔𝑖(1st ‘𝑢) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))) | 
| 149 | 148 | com23 86 | . . . . . . . . . . . . . . . . . 18
⊢
((1st ‘𝑢) ∈ 𝑠 → ((1st ‘𝑡) =
∀𝑔𝑖(1st ‘𝑢) → (𝑖 ∈ ω → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))) | 
| 150 | 149 | a1d 25 | . . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑢) ∈ 𝑠 → (𝑦 ∈ ω → ((1st
‘𝑡) =
∀𝑔𝑖(1st ‘𝑢) → (𝑖 ∈ ω → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))) | 
| 151 | 150 | exlimiv 1929 | . . . . . . . . . . . . . . . 16
⊢
(∃𝑠(1st ‘𝑢) ∈ 𝑠 → (𝑦 ∈ ω → ((1st
‘𝑡) =
∀𝑔𝑖(1st ‘𝑢) → (𝑖 ∈ ω → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))) | 
| 152 | 92, 151 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ ((∅ Sat
∅)‘𝑦) ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑦 ∈ ω → ((1st
‘𝑡) =
∀𝑔𝑖(1st ‘𝑢) → (𝑖 ∈ ω → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))) | 
| 153 | 152 | ex 412 | . . . . . . . . . . . . . 14
⊢ (𝑢 ∈ ((∅ Sat
∅)‘𝑦) →
(∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑦 ∈ ω → ((1st
‘𝑡) =
∀𝑔𝑖(1st ‘𝑢) → (𝑖 ∈ ω → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))))) | 
| 154 | 153 | impcomd 411 | . . . . . . . . . . . . 13
⊢ (𝑢 ∈ ((∅ Sat
∅)‘𝑦) →
((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((1st ‘𝑡) =
∀𝑔𝑖(1st ‘𝑢) → (𝑖 ∈ ω → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))) | 
| 155 | 154 | com24 95 | . . . . . . . . . . . 12
⊢ (𝑢 ∈ ((∅ Sat
∅)‘𝑦) →
(𝑖 ∈ ω →
((1st ‘𝑡)
= ∀𝑔𝑖(1st ‘𝑢) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat
∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))) | 
| 156 | 155 | rexlimdv 3152 | . . . . . . . . . . 11
⊢ (𝑢 ∈ ((∅ Sat
∅)‘𝑦) →
(∃𝑖 ∈ ω
(1st ‘𝑡) =
∀𝑔𝑖(1st ‘𝑢) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat
∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))) | 
| 157 | 130, 156 | jaod 859 | . . . . . . . . . 10
⊢ (𝑢 ∈ ((∅ Sat
∅)‘𝑦) →
((∃𝑣 ∈ ((∅
Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
(1st ‘𝑡) =
∀𝑔𝑖(1st ‘𝑢)) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat
∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))) | 
| 158 | 157 | rexlimiv 3147 | . . . . . . . . 9
⊢
(∃𝑢 ∈
((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
(1st ‘𝑡) =
∀𝑔𝑖(1st ‘𝑢)) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat
∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))) | 
| 159 | 158 | adantl 481 | . . . . . . . 8
⊢
(((2nd ‘𝑡) = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
(1st ‘𝑡) =
∀𝑔𝑖(1st ‘𝑢))) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat
∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))) | 
| 160 |  | eqeq1 2740 | . . . . . . . . . . . . 13
⊢ (𝑥 = (1st ‘𝑡) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔
(1st ‘𝑡) =
((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) | 
| 161 | 160 | rexbidv 3178 | . . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘𝑡) → (∃𝑣 ∈ ((∅ Sat
∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔
∃𝑣 ∈ ((∅
Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) | 
| 162 |  | eqeq1 2740 | . . . . . . . . . . . . 13
⊢ (𝑥 = (1st ‘𝑡) → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ (1st
‘𝑡) =
∀𝑔𝑖(1st ‘𝑢))) | 
| 163 | 162 | rexbidv 3178 | . . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘𝑡) → (∃𝑖 ∈ ω 𝑥 =
∀𝑔𝑖(1st ‘𝑢) ↔ ∃𝑖 ∈ ω (1st ‘𝑡) =
∀𝑔𝑖(1st ‘𝑢))) | 
| 164 | 161, 163 | orbi12d 918 | . . . . . . . . . . 11
⊢ (𝑥 = (1st ‘𝑡) → ((∃𝑣 ∈ ((∅ Sat
∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
(1st ‘𝑡) =
∀𝑔𝑖(1st ‘𝑢)))) | 
| 165 | 164 | rexbidv 3178 | . . . . . . . . . 10
⊢ (𝑥 = (1st ‘𝑡) → (∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ↔ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
(1st ‘𝑡) =
∀𝑔𝑖(1st ‘𝑢)))) | 
| 166 | 165 | anbi2d 630 | . . . . . . . . 9
⊢ (𝑥 = (1st ‘𝑡) → ((𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) ↔ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
(1st ‘𝑡) =
∀𝑔𝑖(1st ‘𝑢))))) | 
| 167 |  | eqeq1 2740 | . . . . . . . . . 10
⊢ (𝑧 = (2nd ‘𝑡) → (𝑧 = ∅ ↔ (2nd
‘𝑡) =
∅)) | 
| 168 | 167 | anbi1d 631 | . . . . . . . . 9
⊢ (𝑧 = (2nd ‘𝑡) → ((𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
(1st ‘𝑡) =
∀𝑔𝑖(1st ‘𝑢))) ↔ ((2nd ‘𝑡) = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
(1st ‘𝑡) =
∀𝑔𝑖(1st ‘𝑢))))) | 
| 169 | 166, 168 | elopabi 8088 | . . . . . . . 8
⊢ (𝑡 ∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} → ((2nd ‘𝑡) = ∅ ∧ ∃𝑢 ∈ ((∅ Sat
∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
(1st ‘𝑡) =
∀𝑔𝑖(1st ‘𝑢)))) | 
| 170 | 159, 169 | syl11 33 | . . . . . . 7
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))} → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))) | 
| 171 | 77, 170 | jaod 859 | . . . . . 6
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((𝑡 ∈ ((∅ Sat ∅)‘𝑦) ∨ 𝑡 ∈ {〈𝑥, 𝑧〉 ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))}) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))) | 
| 172 | 72, 171 | sylbid 240 | . . . . 5
⊢ ((𝑦 ∈ ω ∧
∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘suc
𝑦) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))) | 
| 173 | 172 | ex 412 | . . . 4
⊢ (𝑦 ∈ ω →
(∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑡 ∈ ((∅ Sat ∅)‘suc
𝑦) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))) | 
| 174 | 173 | ralrimdv 3151 | . . 3
⊢ (𝑦 ∈ ω →
(∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → ∀𝑡 ∈ ((∅ Sat ∅)‘suc
𝑦)∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))) | 
| 175 | 75 | cbvralvw 3236 | . . 3
⊢
(∀𝑤 ∈
((∅ Sat ∅)‘suc 𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑡 ∈ ((∅ Sat ∅)‘suc
𝑦)∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))) | 
| 176 | 174, 175 | imbitrrdi 252 | . 2
⊢ (𝑦 ∈ ω →
(∀𝑤 ∈ ((∅
Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → ∀𝑤 ∈ ((∅ Sat ∅)‘suc
𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))) | 
| 177 | 2, 4, 6, 8, 37, 176 | finds 7919 | 1
⊢ (𝑁 ∈ ω →
∀𝑤 ∈ ((∅
Sat ∅)‘𝑁)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) |