Theorem sat1el2xp 35573

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 6834	. . 3 ⊢ (𝑥 = ∅ → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘∅))
2	1	raleqdv 3296	. 2 ⊢ (𝑥 = ∅ → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘∅)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
3		fveq2 6834	. . 3 ⊢ (𝑥 = 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘𝑦))
4	3	raleqdv 3296	. 2 ⊢ (𝑥 = 𝑦 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
5		fveq2 6834	. . 3 ⊢ (𝑥 = suc 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘suc 𝑦))
6	5	raleqdv 3296	. 2 ⊢ (𝑥 = suc 𝑦 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
7		fveq2 6834	. . 3 ⊢ (𝑥 = 𝑁 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘𝑁))
8	7	raleqdv 3296	. 2 ⊢ (𝑥 = 𝑁 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑁)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
9		eqeq1 2740	. . . . . . . 8 ⊢ (𝑥 = (1st ‘𝑤) → (𝑥 = (𝑖∈𝑔𝑗) ↔ (1st ‘𝑤) = (𝑖∈𝑔𝑗)))
10	9	2rexbidv 3201	. . . . . . 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 8006	. . . . 5 ⊢ (𝑤 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} → ((2nd ‘𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)))
15		goel 35541	. . . . . . . . 9 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖∈𝑔𝑗) = ⟨∅, ⟨𝑖, 𝑗⟩⟩)
16	15	eqeq2d 2747	. . . . . . . 8 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((1st ‘𝑤) = (𝑖∈𝑔𝑗) ↔ (1st ‘𝑤) = ⟨∅, ⟨𝑖, 𝑗⟩⟩))
17		omex 9552	. . . . . . . . . . 11 ⊢ ω ∈ V
18	17, 17	pm3.2i 470	. . . . . . . . . 10 ⊢ (ω ∈ V ∧ ω ∈ V)
19		peano1 7831	. . . . . . . . . . . 12 ⊢ ∅ ∈ ω
20	19	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ∅ ∈ ω)
21		opelxpi 5661	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ⟨𝑖, 𝑗⟩ ∈ (ω × ω))
22	20, 21	opelxpd 5663	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (ω × ω)))
23		xpeq12 5649	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ω ∧ 𝑏 = ω) → (𝑎 × 𝑏) = (ω × ω))
24	23	xpeq2d 5654	. . . . . . . . . . . 12 ⊢ ((𝑎 = ω ∧ 𝑏 = ω) → (ω × (𝑎 × 𝑏)) = (ω × (ω × ω)))
25	24	eleq2d 2822	. . . . . . . . . . 11 ⊢ ((𝑎 = ω ∧ 𝑏 = ω) → (⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏)) ↔ ⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (ω × ω))))
26	25	spc2egv 3553	. . . . . . . . . 10 ⊢ ((ω ∈ V ∧ ω ∈ V) → (⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (ω × ω)) → ∃𝑎∃𝑏⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏))))
27	18, 22, 26	mpsyl 68	. . . . . . . . 9 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ∃𝑎∃𝑏⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏)))
28		eleq1 2824	. . . . . . . . . 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 3178	. . . . . 6 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
33	32	adantl 481	. . . . 5 ⊢ (((2nd ‘𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
34	14, 33	syl 17	. . . 4 ⊢ (𝑤 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
35		satf00 35568	. . . 4 ⊢ ((∅ Sat ∅)‘∅) = {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))}
36	34, 35	eleq2s 2854	. . 3 ⊢ (𝑤 ∈ ((∅ Sat ∅)‘∅) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
37	36	rgen 3053	. 2 ⊢ ∀𝑤 ∈ ((∅ Sat ∅)‘∅)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))
38		omsucelsucb 8389	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈ suc ω)
39		satf0sucom 35567	. . . . . . . . . . 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 7814	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ω → 𝑦 ∈ On)
43		rdgsuc 8355	. . . . . . . . . . . 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 6392	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ω → 𝑦 ∈ suc ω)
47		satf0sucom 35567	. . . . . . . . . . . . . 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 6838	. . . . . . . . . . 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 3292	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ ∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
55	54	orbi1d 916	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → ((∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))
56	55	rexeqbi1dv 3309	. . . . . . . . . . . . . . 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 5164	. . . . . . . . . . . . 13 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))} = {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})
59	53, 58	uneq12d 4121	. . . . . . . . . . . 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 6849	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((∅ Sat ∅)‘𝑦) ∈ V)
62	17	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ω ∈ V)
63		satf0suclem 35569	. . . . . . . . . . . . 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 7688	. . . . . . . . . . . 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 6948	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))‘((∅ Sat ∅)‘𝑦)) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))
68	45, 51, 67	3eqtrd 2775	. . . . . . . . 9 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑦) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))
69	41, 68	eqtrd 2771	. . . . . . . 8 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((∅ Sat ∅)‘suc 𝑦) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))
70	69	eleq2d 2822	. . . . . . 7 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦) ↔ 𝑡 ∈ (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})))
71		elun 4105	. . . . . . 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 6834	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑡 → (1st ‘𝑤) = (1st ‘𝑡))
74	73	eleq1d 2821	. . . . . . . . . 10 ⊢ (𝑤 = 𝑡 → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
75	74	2exbidv 1925	. . . . . . . . 9 ⊢ (𝑤 = 𝑡 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
76	75	rspccv 3573	. . . . . . . 8 ⊢ (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑡 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
77	76	adantl 481	. . . . . . 7 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
78		fveq2 6834	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑣 → (1st ‘𝑤) = (1st ‘𝑣))
79	78	eleq1d 2821	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑣 → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏))))
80	79	2exbidv 1925	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑣 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏(1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏))))
81	80	rspcva 3574	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏)))
82		sels 5388	. . . . . . . . . . . . . . . . . 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 6834	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑢 → (1st ‘𝑤) = (1st ‘𝑢))
87	86	eleq1d 2821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑢 → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏))))
88	87	2exbidv 1925	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑢 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏(1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏))))
89	88	rspcva 3574	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)))
90		sels 5388	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑢) ∈ 𝑠)
91	90	exlimivv 1933	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑎∃𝑏(1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑢) ∈ 𝑠)
92	89, 91	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑠(1st ‘𝑢) ∈ 𝑠)
93		eleq2w 2820	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 𝑟 → ((1st ‘𝑢) ∈ 𝑠 ↔ (1st ‘𝑢) ∈ 𝑟))
94	93	cbvexvw 2038	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑠(1st ‘𝑢) ∈ 𝑠 ↔ ∃𝑟(1st ‘𝑢) ∈ 𝑟)
95		vex 3444	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑟 ∈ V
96		vex 3444	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑠 ∈ V
97	95, 96	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑟 ∈ V ∧ 𝑠 ∈ V)
98		df-ov 7361	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) = (⊼𝑔‘⟨(1st ‘𝑢), (1st ‘𝑣)⟩)
99		df-gona 35535	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ⊼𝑔 = (𝑒 ∈ (V × V) ↦ ⟨1o, 𝑒⟩)
100		opeq2 4830	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑒 = ⟨(1st ‘𝑢), (1st ‘𝑣)⟩ → ⟨1o, 𝑒⟩ = ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩)
101		opelvvg 5665	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨(1st ‘𝑢), (1st ‘𝑣)⟩ ∈ (V × V))
102		opex 5412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩ ∈ V
103	102	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩ ∈ V)
104	99, 100, 101, 103	fvmptd3 6964	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → (⊼𝑔‘⟨(1st ‘𝑢), (1st ‘𝑣)⟩) = ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩)
105	98, 104	eqtrid 2783	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) = ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩)
106		1onn 8568	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 1o ∈ ω
107	106	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → 1o ∈ ω)
108		opelxpi 5661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨(1st ‘𝑢), (1st ‘𝑣)⟩ ∈ (𝑟 × 𝑠))
109	107, 108	opelxpd 5663	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩ ∈ (ω × (𝑟 × 𝑠)))
110	105, 109	eqeltrd 2836	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑟 × 𝑠)))
111		xpeq12 5649	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 = 𝑟 ∧ 𝑏 = 𝑠) → (𝑎 × 𝑏) = (𝑟 × 𝑠))
112	111	xpeq2d 5654	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 = 𝑟 ∧ 𝑏 = 𝑠) → (ω × (𝑎 × 𝑏)) = (ω × (𝑟 × 𝑠)))
113	112	eleq2d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 = 𝑟 ∧ 𝑏 = 𝑠) → (((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑎 × 𝑏)) ↔ ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑟 × 𝑠))))
114	113	spc2egv 3553	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑟 ∈ V ∧ 𝑠 ∈ V) → (((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑟 × 𝑠)) → ∃𝑎∃𝑏((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑎 × 𝑏))))
115	97, 110, 114	mpsyl 68	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ∃𝑎∃𝑏((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑎 × 𝑏)))
116		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . . 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 3135	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))
131	17, 96	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ω ∈ V ∧ 𝑠 ∈ V)
132		df-goal 35536	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∀𝑔𝑖(1st ‘𝑢) = ⟨2o, ⟨𝑖, (1st ‘𝑢)⟩⟩
133		2onn 8570	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2o ∈ ω
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → 2o ∈ ω)
135		opelxpi 5661	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑖 ∈ ω ∧ (1st ‘𝑢) ∈ 𝑠) → ⟨𝑖, (1st ‘𝑢)⟩ ∈ (ω × 𝑠))
136	135	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → ⟨𝑖, (1st ‘𝑢)⟩ ∈ (ω × 𝑠))
137	134, 136	opelxpd 5663	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → ⟨2o, ⟨𝑖, (1st ‘𝑢)⟩⟩ ∈ (ω × (ω × 𝑠)))
138	132, 137	eqeltrid 2840	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → ∀𝑔𝑖(1st ‘𝑢) ∈ (ω × (ω × 𝑠)))
139	138	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω ∧ (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)) → ∀𝑔𝑖(1st ‘𝑢) ∈ (ω × (ω × 𝑠)))
140		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . 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 5649	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 = ω ∧ 𝑏 = 𝑠) → (𝑎 × 𝑏) = (ω × 𝑠))
144	143	xpeq2d 5654	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 = ω ∧ 𝑏 = 𝑠) → (ω × (𝑎 × 𝑏)) = (ω × (ω × 𝑠)))
145	144	eleq2d 2822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 = ω ∧ 𝑏 = 𝑠) → ((1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑡) ∈ (ω × (ω × 𝑠))))
146	145	spc2egv 3553	. . . . . . . . . . . . . . . . . . . . 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 3135	. . . . . . . . . . 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 3130	. . . . . . . . 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 3160	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘𝑡) → (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ ∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
162		eqeq1 2740	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1st ‘𝑡) → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)))
163	162	rexbidv 3160	. . . . . . . . . . . 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 3160	. . . . . . . . . 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 8006	. . . . . . . 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 3134	. . 3 ⊢ (𝑦 ∈ ω → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → ∀𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
175	75	cbvralvw 3214	. . 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 7838	1 ⊢ (𝑁 ∈ ω → ∀𝑤 ∈ ((∅ Sat ∅)‘𝑁)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∀wral 3051  ∃wrex 3060  Vcvv 3440   ∪ cun 3899  ∅c0 4285  ⟨cop 4586  {copab 5160   ↦ cmpt 5179   × cxp 5622  Oncon0 6317  suc csuc 6319  ‘cfv 6492  (class class class)co 7358  ωcom 7808  1^st c1st 7931  2^nd c2nd 7932  reccrdg 8340  1_oc1o 8390  2_oc2o 8391  ∈_𝑔cgoe 35527  ⊼_𝑔cgna 35528  ∀_𝑔cgol 35529   Sat csat 35530

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-inf2 9550

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-2o 8398  df-map 8765  df-goel 35534  df-gona 35535  df-goal 35536  df-sat 35537

This theorem is referenced by: (None)