Theorem sat1el2xp 35411

Description: The first component of an element of the value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation is a member of a doubled Cartesian product. (Contributed by AV, 17-Sep-2023.)

Assertion

Ref	Expression
sat1el2xp	⊢ (𝑁 ∈ ω → ∀𝑤 ∈ ((∅ Sat ∅)‘𝑁)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))

Distinct variable groups:   𝑤,𝑁   𝑎,𝑏,𝑤

Allowed substitution hints:   𝑁(𝑎,𝑏)

Proof of Theorem sat1el2xp

Dummy variables 𝑥 𝑓 𝑖 𝑗 𝑢 𝑣 𝑟 𝑠 𝑡 𝑦 𝑒 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6822	. . 3 ⊢ (𝑥 = ∅ → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘∅))
2	1	raleqdv 3292	. 2 ⊢ (𝑥 = ∅ → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘∅)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
3		fveq2 6822	. . 3 ⊢ (𝑥 = 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘𝑦))
4	3	raleqdv 3292	. 2 ⊢ (𝑥 = 𝑦 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
5		fveq2 6822	. . 3 ⊢ (𝑥 = suc 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘suc 𝑦))
6	5	raleqdv 3292	. 2 ⊢ (𝑥 = suc 𝑦 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
7		fveq2 6822	. . 3 ⊢ (𝑥 = 𝑁 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘𝑁))
8	7	raleqdv 3292	. 2 ⊢ (𝑥 = 𝑁 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑁)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
9		eqeq1 2735	. . . . . . . 8 ⊢ (𝑥 = (1st ‘𝑤) → (𝑥 = (𝑖∈𝑔𝑗) ↔ (1st ‘𝑤) = (𝑖∈𝑔𝑗)))
10	9	2rexbidv 3197	. . . . . . 7 ⊢ (𝑥 = (1st ‘𝑤) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)))
11	10	anbi2d 630	. . . . . 6 ⊢ (𝑥 = (1st ‘𝑤) → ((𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) ↔ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗))))
12		eqeq1 2735	. . . . . . 7 ⊢ (𝑧 = (2nd ‘𝑤) → (𝑧 = ∅ ↔ (2nd ‘𝑤) = ∅))
13	12	anbi1d 631	. . . . . 6 ⊢ (𝑧 = (2nd ‘𝑤) → ((𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)) ↔ ((2nd ‘𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗))))
14	11, 13	elopabi 7994	. . . . 5 ⊢ (𝑤 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} → ((2nd ‘𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)))
15		goel 35379	. . . . . . . . 9 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖∈𝑔𝑗) = ⟨∅, ⟨𝑖, 𝑗⟩⟩)
16	15	eqeq2d 2742	. . . . . . . 8 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((1st ‘𝑤) = (𝑖∈𝑔𝑗) ↔ (1st ‘𝑤) = ⟨∅, ⟨𝑖, 𝑗⟩⟩))
17		omex 9533	. . . . . . . . . . 11 ⊢ ω ∈ V
18	17, 17	pm3.2i 470	. . . . . . . . . 10 ⊢ (ω ∈ V ∧ ω ∈ V)
19		peano1 7819	. . . . . . . . . . . 12 ⊢ ∅ ∈ ω
20	19	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ∅ ∈ ω)
21		opelxpi 5653	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ⟨𝑖, 𝑗⟩ ∈ (ω × ω))
22	20, 21	opelxpd 5655	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (ω × ω)))
23		xpeq12 5641	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ω ∧ 𝑏 = ω) → (𝑎 × 𝑏) = (ω × ω))
24	23	xpeq2d 5646	. . . . . . . . . . . 12 ⊢ ((𝑎 = ω ∧ 𝑏 = ω) → (ω × (𝑎 × 𝑏)) = (ω × (ω × ω)))
25	24	eleq2d 2817	. . . . . . . . . . 11 ⊢ ((𝑎 = ω ∧ 𝑏 = ω) → (⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏)) ↔ ⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (ω × ω))))
26	25	spc2egv 3554	. . . . . . . . . 10 ⊢ ((ω ∈ V ∧ ω ∈ V) → (⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (ω × ω)) → ∃𝑎∃𝑏⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏))))
27	18, 22, 26	mpsyl 68	. . . . . . . . 9 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ∃𝑎∃𝑏⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏)))
28		eleq1 2819	. . . . . . . . . 10 ⊢ ((1st ‘𝑤) = ⟨∅, ⟨𝑖, 𝑗⟩⟩ → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏))))
29	28	2exbidv 1925	. . . . . . . . 9 ⊢ ((1st ‘𝑤) = ⟨∅, ⟨𝑖, 𝑗⟩⟩ → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏))))
30	27, 29	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((1st ‘𝑤) = ⟨∅, ⟨𝑖, 𝑗⟩⟩ → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
31	16, 30	sylbid 240	. . . . . . 7 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((1st ‘𝑤) = (𝑖∈𝑔𝑗) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
32	31	rexlimivv 3174	. . . . . 6 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
33	32	adantl 481	. . . . 5 ⊢ (((2nd ‘𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
34	14, 33	syl 17	. . . 4 ⊢ (𝑤 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
35		satf00 35406	. . . 4 ⊢ ((∅ Sat ∅)‘∅) = {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))}
36	34, 35	eleq2s 2849	. . 3 ⊢ (𝑤 ∈ ((∅ Sat ∅)‘∅) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
37	36	rgen 3049	. 2 ⊢ ∀𝑤 ∈ ((∅ Sat ∅)‘∅)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))
38		omsucelsucb 8377	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈ suc ω)
39		satf0sucom 35405	. . . . . . . . . . 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 7802	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ω → 𝑦 ∈ On)
43		rdgsuc 8343	. . . . . . . . . . . 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 6381	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ω → 𝑦 ∈ suc ω)
47		satf0sucom 35405	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ suc ω → ((∅ Sat ∅)‘𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦))
48	46, 47	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ω → ((∅ Sat ∅)‘𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦))
49	48	eqcomd 2737	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ω → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦) = ((∅ Sat ∅)‘𝑦))
50	49	fveq2d 6826	. . . . . . . . . . 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 2732	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})) = (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})))
53		id 22	. . . . . . . . . . . . 13 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → 𝑓 = ((∅ Sat ∅)‘𝑦))
54		rexeq 3288	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ ∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
55	54	orbi1d 916	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → ((∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))
56	55	rexeqbi1dv 3305	. . . . . . . . . . . . . . 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 5157	. . . . . . . . . . . . 13 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))} = {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})
59	53, 58	uneq12d 4119	. . . . . . . . . . . 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 6837	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((∅ Sat ∅)‘𝑦) ∈ V)
62	17	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ω ∈ V)
63		satf0suclem 35407	. . . . . . . . . . . . 13 ⊢ ((((∅ Sat ∅)‘𝑦) ∈ V ∧ ((∅ Sat ∅)‘𝑦) ∈ V ∧ ω ∈ V) → {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))} ∈ V)
64	61, 61, 62, 63	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))} ∈ V)
65		unexg 7676	. . . . . . . . . . . 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 6936	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))‘((∅ Sat ∅)‘𝑦)) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))
68	45, 51, 67	3eqtrd 2770	. . . . . . . . 9 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑦) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))
69	41, 68	eqtrd 2766	. . . . . . . 8 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((∅ Sat ∅)‘suc 𝑦) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))
70	69	eleq2d 2817	. . . . . . 7 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦) ↔ 𝑡 ∈ (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})))
71		elun 4103	. . . . . . 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 6822	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑡 → (1st ‘𝑤) = (1st ‘𝑡))
74	73	eleq1d 2816	. . . . . . . . . 10 ⊢ (𝑤 = 𝑡 → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
75	74	2exbidv 1925	. . . . . . . . 9 ⊢ (𝑤 = 𝑡 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
76	75	rspccv 3574	. . . . . . . 8 ⊢ (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑡 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
77	76	adantl 481	. . . . . . 7 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
78		fveq2 6822	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑣 → (1st ‘𝑤) = (1st ‘𝑣))
79	78	eleq1d 2816	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑣 → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏))))
80	79	2exbidv 1925	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑣 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏(1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏))))
81	80	rspcva 3575	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏)))
82		sels 5381	. . . . . . . . . . . . . . . . . 18 ⊢ ((1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑣) ∈ 𝑠)
83	82	exlimivv 1933	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑎∃𝑏(1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑣) ∈ 𝑠)
84	81, 83	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑠(1st ‘𝑣) ∈ 𝑠)
85	84	expcom 413	. . . . . . . . . . . . . . 15 ⊢ (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑣 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑠(1st ‘𝑣) ∈ 𝑠))
86		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑢 → (1st ‘𝑤) = (1st ‘𝑢))
87	86	eleq1d 2816	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑢 → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏))))
88	87	2exbidv 1925	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑢 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏(1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏))))
89	88	rspcva 3575	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)))
90		sels 5381	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑢) ∈ 𝑠)
91	90	exlimivv 1933	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑎∃𝑏(1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑢) ∈ 𝑠)
92	89, 91	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑠(1st ‘𝑢) ∈ 𝑠)
93		eleq2w 2815	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 𝑟 → ((1st ‘𝑢) ∈ 𝑠 ↔ (1st ‘𝑢) ∈ 𝑟))
94	93	cbvexvw 2038	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑠(1st ‘𝑢) ∈ 𝑠 ↔ ∃𝑟(1st ‘𝑢) ∈ 𝑟)
95		vex 3440	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑟 ∈ V
96		vex 3440	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑠 ∈ V
97	95, 96	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑟 ∈ V ∧ 𝑠 ∈ V)
98		df-ov 7349	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) = (⊼𝑔‘⟨(1st ‘𝑢), (1st ‘𝑣)⟩)
99		df-gona 35373	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ⊼𝑔 = (𝑒 ∈ (V × V) ↦ ⟨1o, 𝑒⟩)
100		opeq2 4826	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑒 = ⟨(1st ‘𝑢), (1st ‘𝑣)⟩ → ⟨1o, 𝑒⟩ = ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩)
101		opelvvg 5657	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨(1st ‘𝑢), (1st ‘𝑣)⟩ ∈ (V × V))
102		opex 5404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩ ∈ V
103	102	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩ ∈ V)
104	99, 100, 101, 103	fvmptd3 6952	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → (⊼𝑔‘⟨(1st ‘𝑢), (1st ‘𝑣)⟩) = ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩)
105	98, 104	eqtrid 2778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) = ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩)
106		1onn 8555	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 1o ∈ ω
107	106	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → 1o ∈ ω)
108		opelxpi 5653	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨(1st ‘𝑢), (1st ‘𝑣)⟩ ∈ (𝑟 × 𝑠))
109	107, 108	opelxpd 5655	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩ ∈ (ω × (𝑟 × 𝑠)))
110	105, 109	eqeltrd 2831	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑟 × 𝑠)))
111		xpeq12 5641	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 = 𝑟 ∧ 𝑏 = 𝑠) → (𝑎 × 𝑏) = (𝑟 × 𝑠))
112	111	xpeq2d 5646	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 = 𝑟 ∧ 𝑏 = 𝑠) → (ω × (𝑎 × 𝑏)) = (ω × (𝑟 × 𝑠)))
113	112	eleq2d 2817	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 = 𝑟 ∧ 𝑏 = 𝑠) → (((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑎 × 𝑏)) ↔ ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑟 × 𝑠))))
114	113	spc2egv 3554	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑟 ∈ V ∧ 𝑠 ∈ V) → (((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑟 × 𝑠)) → ∃𝑎∃𝑏((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑎 × 𝑏))))
115	97, 110, 114	mpsyl 68	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ∃𝑎∃𝑏((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑎 × 𝑏)))
116		eleq1 2819	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) → ((1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)) ↔ ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑎 × 𝑏))))
117	116	2exbidv 1925	. . . . . . . . . . . . . . . . . . . . . . . 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 1934	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1st ‘𝑢) ∈ 𝑟 → (∃𝑠(1st ‘𝑣) ∈ 𝑠 → ((1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))
121	120	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1st ‘𝑢) ∈ 𝑟 → ((1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) → (∃𝑠(1st ‘𝑣) ∈ 𝑠 → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))
122	121	exlimiv 1931	. . . . . . . . . . . . . . . . . . 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 3131	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))
131	17, 96	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ω ∈ V ∧ 𝑠 ∈ V)
132		df-goal 35374	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∀𝑔𝑖(1st ‘𝑢) = ⟨2o, ⟨𝑖, (1st ‘𝑢)⟩⟩
133		2onn 8557	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2o ∈ ω
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → 2o ∈ ω)
135		opelxpi 5653	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑖 ∈ ω ∧ (1st ‘𝑢) ∈ 𝑠) → ⟨𝑖, (1st ‘𝑢)⟩ ∈ (ω × 𝑠))
136	135	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → ⟨𝑖, (1st ‘𝑢)⟩ ∈ (ω × 𝑠))
137	134, 136	opelxpd 5655	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → ⟨2o, ⟨𝑖, (1st ‘𝑢)⟩⟩ ∈ (ω × (ω × 𝑠)))
138	132, 137	eqeltrid 2835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → ∀𝑔𝑖(1st ‘𝑢) ∈ (ω × (ω × 𝑠)))
139	138	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω ∧ (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)) → ∀𝑔𝑖(1st ‘𝑢) ∈ (ω × (ω × 𝑠)))
140		eleq1 2819	. . . . . . . . . . . . . . . . . . . . . . 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 5641	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 = ω ∧ 𝑏 = 𝑠) → (𝑎 × 𝑏) = (ω × 𝑠))
144	143	xpeq2d 5646	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 = ω ∧ 𝑏 = 𝑠) → (ω × (𝑎 × 𝑏)) = (ω × (ω × 𝑠)))
145	144	eleq2d 2817	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 = ω ∧ 𝑏 = 𝑠) → ((1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑡) ∈ (ω × (ω × 𝑠))))
146	145	spc2egv 3554	. . . . . . . . . . . . . . . . . . . . 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 1931	. . . . . . . . . . . . . . . 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 3131	. . . . . . . . . . 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 3126	. . . . . . . . 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 2735	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1st ‘𝑡) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ (1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
161	160	rexbidv 3156	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘𝑡) → (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ ∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
162		eqeq1 2735	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1st ‘𝑡) → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)))
163	162	rexbidv 3156	. . . . . . . . . . . 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 3156	. . . . . . . . . 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 2735	. . . . . . . . . 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 7994	. . . . . . . 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 3130	. . 3 ⊢ (𝑦 ∈ ω → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → ∀𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
175	75	cbvralvw 3210	. . 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 7826	1 ⊢ (𝑁 ∈ ω → ∀𝑤 ∈ ((∅ Sat ∅)‘𝑁)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056  Vcvv 3436   ∪ cun 3900  ∅c0 4283  ⟨cop 4582  {copab 5153   ↦ cmpt 5172   × cxp 5614  Oncon0 6306  suc csuc 6308  ‘cfv 6481  (class class class)co 7346  ωcom 7796  1^st c1st 7919  2^nd c2nd 7920  reccrdg 8328  1_oc1o 8378  2_oc2o 8379  ∈_𝑔cgoe 35365  ⊼_𝑔cgna 35366  ∀_𝑔cgol 35367   Sat csat 35368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5217  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-inf2 9531

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7797  df-1st 7921  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-1o 8385  df-2o 8386  df-map 8752  df-goel 35372  df-gona 35373  df-goal 35374  df-sat 35375

This theorem is referenced by: (None)