Theorem sat1el2xp 35614

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 3298	. 2 ⊢ (𝑥 = ∅ → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘∅)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
3		fveq2 6834	. . 3 ⊢ (𝑥 = 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘𝑦))
4	3	raleqdv 3298	. 2 ⊢ (𝑥 = 𝑦 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
5		fveq2 6834	. . 3 ⊢ (𝑥 = suc 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘suc 𝑦))
6	5	raleqdv 3298	. 2 ⊢ (𝑥 = suc 𝑦 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
7		fveq2 6834	. . 3 ⊢ (𝑥 = 𝑁 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘𝑁))
8	7	raleqdv 3298	. 2 ⊢ (𝑥 = 𝑁 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑁)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
9		eqeq1 2744	. . . . . . . 8 ⊢ (𝑥 = (1st ‘𝑤) → (𝑥 = (𝑖∈𝑔𝑗) ↔ (1st ‘𝑤) = (𝑖∈𝑔𝑗)))
10	9	2rexbidv 3205	. . . . . . 7 ⊢ (𝑥 = (1st ‘𝑤) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)))
11	10	anbi2d 636	. . . . . 6 ⊢ (𝑥 = (1st ‘𝑤) → ((𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) ↔ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗))))
12		eqeq1 2744	. . . . . . 7 ⊢ (𝑧 = (2nd ‘𝑤) → (𝑧 = ∅ ↔ (2nd ‘𝑤) = ∅))
13	12	anbi1d 637	. . . . . 6 ⊢ (𝑧 = (2nd ‘𝑤) → ((𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)) ↔ ((2nd ‘𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗))))
14	11, 13	elopabi 8011	. . . . 5 ⊢ (𝑤 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} → ((2nd ‘𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)))
15		goel 35582	. . . . . . . . 9 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖∈𝑔𝑗) = ⟨∅, ⟨𝑖, 𝑗⟩⟩)
16	15	eqeq2d 2751	. . . . . . . 8 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((1st ‘𝑤) = (𝑖∈𝑔𝑗) ↔ (1st ‘𝑤) = ⟨∅, ⟨𝑖, 𝑗⟩⟩))
17		omex 9562	. . . . . . . . . . 11 ⊢ ω ∈ V
18	17, 17	pm3.2i 471	. . . . . . . . . 10 ⊢ (ω ∈ V ∧ ω ∈ V)
19		peano1 7836	. . . . . . . . . . . 12 ⊢ ∅ ∈ ω
20	19	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ∅ ∈ ω)
21		opelxpi 5662	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ⟨𝑖, 𝑗⟩ ∈ (ω × ω))
22	20, 21	opelxpd 5664	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (ω × ω)))
23		xpeq12 5650	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ω ∧ 𝑏 = ω) → (𝑎 × 𝑏) = (ω × ω))
24	23	xpeq2d 5655	. . . . . . . . . . . 12 ⊢ ((𝑎 = ω ∧ 𝑏 = ω) → (ω × (𝑎 × 𝑏)) = (ω × (ω × ω)))
25	24	eleq2d 2826	. . . . . . . . . . 11 ⊢ ((𝑎 = ω ∧ 𝑏 = ω) → (⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏)) ↔ ⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (ω × ω))))
26	25	spc2egv 3544	. . . . . . . . . 10 ⊢ ((ω ∈ V ∧ ω ∈ V) → (⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (ω × ω)) → ∃𝑎∃𝑏⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏))))
27	18, 22, 26	mpsyl 68	. . . . . . . . 9 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ∃𝑎∃𝑏⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏)))
28		eleq1 2828	. . . . . . . . . 10 ⊢ ((1st ‘𝑤) = ⟨∅, ⟨𝑖, 𝑗⟩⟩ → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏))))
29	28	2exbidv 1931	. . . . . . . . 9 ⊢ ((1st ‘𝑤) = ⟨∅, ⟨𝑖, 𝑗⟩⟩ → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏))))
30	27, 29	syl5ibrcom 248	. . . . . . . 8 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((1st ‘𝑤) = ⟨∅, ⟨𝑖, 𝑗⟩⟩ → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
31	16, 30	sylbid 241	. . . . . . 7 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((1st ‘𝑤) = (𝑖∈𝑔𝑗) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
32	31	rexlimivv 3182	. . . . . 6 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
33	32	adantl 482	. . . . 5 ⊢ (((2nd ‘𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
34	14, 33	syl 17	. . . 4 ⊢ (𝑤 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
35		satf00 35609	. . . 4 ⊢ ((∅ Sat ∅)‘∅) = {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))}
36	34, 35	eleq2s 2858	. . 3 ⊢ (𝑤 ∈ ((∅ Sat ∅)‘∅) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
37	36	rgen 3056	. 2 ⊢ ∀𝑤 ∈ ((∅ Sat ∅)‘∅)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))
38		omsucelsucb 8394	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈ suc ω)
39		satf0sucom 35608	. . . . . . . . . . 11 ⊢ (suc 𝑦 ∈ suc ω → ((∅ Sat ∅)‘suc 𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑦))
40	38, 39	sylbi 218	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → ((∅ Sat ∅)‘suc 𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑦))
41	40	adantr 481	. . . . . . . . 9 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((∅ Sat ∅)‘suc 𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑦))
42		nnon 7819	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ω → 𝑦 ∈ On)
43		rdgsuc 8360	. . . . . . . . . . . 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 481	. . . . . . . . . 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 35608	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ suc ω → ((∅ Sat ∅)‘𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦))
48	46, 47	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ω → ((∅ Sat ∅)‘𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦))
49	48	eqcomd 2746	. . . . . . . . . . . 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 481	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦)) = ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))‘((∅ Sat ∅)‘𝑦)))
52		eqidd 2741	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})) = (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})))
53		id 22	. . . . . . . . . . . . 13 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → 𝑓 = ((∅ Sat ∅)‘𝑦))
54		rexeq 3294	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ ∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
55	54	orbi1d 922	. . . . . . . . . . . . . . . 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 636	. . . . . . . . . . . . . 14 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → ((𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))) ↔ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))))
58	57	opabbidv 5145	. . . . . . . . . . . . 13 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))} = {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})
59	53, 58	uneq12d 4106	. . . . . . . . . . . 12 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))
60	59	adantl 482	. . . . . . . . . . 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 35610	. . . . . . . . . . . . 13 ⊢ ((((∅ Sat ∅)‘𝑦) ∈ V ∧ ((∅ Sat ∅)‘𝑦) ∈ V ∧ ω ∈ V) → {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))} ∈ V)
64	61, 61, 62, 63	syl3anc 1379	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))} ∈ V)
65		unexg 7693	. . . . . . . . . . . 12 ⊢ ((((∅ Sat ∅)‘𝑦) ∈ V ∧ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))} ∈ V) → (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}) ∈ V)
66	61, 64, 65	syl2anc 590	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}) ∈ V)
67	52, 60, 61, 66	fvmptd 6950	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))‘((∅ Sat ∅)‘𝑦)) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))
68	45, 51, 67	3eqtrd 2779	. . . . . . . . 9 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑦) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))
69	41, 68	eqtrd 2775	. . . . . . . 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 4090	. . . . . . 7 ⊢ (𝑡 ∈ (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}) ↔ (𝑡 ∈ ((∅ Sat ∅)‘𝑦) ∨ 𝑡 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))
72	70, 71	bitrdi 288	. . . . . 6 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦) ↔ (𝑡 ∈ ((∅ Sat ∅)‘𝑦) ∨ 𝑡 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})))
73		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑡 → (1st ‘𝑤) = (1st ‘𝑡))
74	73	eleq1d 2825	. . . . . . . . . 10 ⊢ (𝑤 = 𝑡 → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
75	74	2exbidv 1931	. . . . . . . . 9 ⊢ (𝑤 = 𝑡 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
76	75	rspccv 3564	. . . . . . . 8 ⊢ (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑡 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
77	76	adantl 482	. . . . . . 7 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
78		fveq2 6834	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑣 → (1st ‘𝑤) = (1st ‘𝑣))
79	78	eleq1d 2825	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑣 → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏))))
80	79	2exbidv 1931	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑣 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏(1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏))))
81	80	rspcva 3565	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏)))
82		sels 5386	. . . . . . . . . . . . . . . . . 18 ⊢ ((1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑣) ∈ 𝑠)
83	82	exlimivv 1939	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑎∃𝑏(1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑣) ∈ 𝑠)
84	81, 83	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑠(1st ‘𝑣) ∈ 𝑠)
85	84	expcom 414	. . . . . . . . . . . . . . 15 ⊢ (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑣 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑠(1st ‘𝑣) ∈ 𝑠))
86		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑢 → (1st ‘𝑤) = (1st ‘𝑢))
87	86	eleq1d 2825	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑢 → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏))))
88	87	2exbidv 1931	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑢 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏(1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏))))
89	88	rspcva 3565	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)))
90		sels 5386	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑢) ∈ 𝑠)
91	90	exlimivv 1939	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑎∃𝑏(1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑢) ∈ 𝑠)
92	89, 91	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑠(1st ‘𝑢) ∈ 𝑠)
93		eleq2w 2824	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 𝑟 → ((1st ‘𝑢) ∈ 𝑠 ↔ (1st ‘𝑢) ∈ 𝑟))
94	93	cbvexvw 2044	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑠(1st ‘𝑢) ∈ 𝑠 ↔ ∃𝑟(1st ‘𝑢) ∈ 𝑟)
95		vex 3436	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑟 ∈ V
96		vex 3436	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑠 ∈ V
97	95, 96	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑟 ∈ V ∧ 𝑠 ∈ V)
98		df-ov 7366	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) = (⊼𝑔‘⟨(1st ‘𝑢), (1st ‘𝑣)⟩)
99		df-gona 35576	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ⊼𝑔 = (𝑒 ∈ (V × V) ↦ ⟨1o, 𝑒⟩)
100		opeq2 4812	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑒 = ⟨(1st ‘𝑢), (1st ‘𝑣)⟩ → ⟨1o, 𝑒⟩ = ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩)
101		opelvvg 5666	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨(1st ‘𝑢), (1st ‘𝑣)⟩ ∈ (V × V))
102		opex 5410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩ ∈ V
103	102	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩ ∈ V)
104	99, 100, 101, 103	fvmptd3 6966	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → (⊼𝑔‘⟨(1st ‘𝑢), (1st ‘𝑣)⟩) = ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩)
105	98, 104	eqtrid 2787	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) = ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩)
106		1onn 8573	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 1o ∈ ω
107	106	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → 1o ∈ ω)
108		opelxpi 5662	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨(1st ‘𝑢), (1st ‘𝑣)⟩ ∈ (𝑟 × 𝑠))
109	107, 108	opelxpd 5664	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩ ∈ (ω × (𝑟 × 𝑠)))
110	105, 109	eqeltrd 2840	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑟 × 𝑠)))
111		xpeq12 5650	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 = 𝑟 ∧ 𝑏 = 𝑠) → (𝑎 × 𝑏) = (𝑟 × 𝑠))
112	111	xpeq2d 5655	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 = 𝑟 ∧ 𝑏 = 𝑠) → (ω × (𝑎 × 𝑏)) = (ω × (𝑟 × 𝑠)))
113	112	eleq2d 2826	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 = 𝑟 ∧ 𝑏 = 𝑠) → (((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑎 × 𝑏)) ↔ ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑟 × 𝑠))))
114	113	spc2egv 3544	. . . . . . . . . . . . . . . . . . . . . . . . 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 1931	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) → (∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑎 × 𝑏))))
118	115, 117	syl5ibrcom 248	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ((1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
119	118	ex 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1st ‘𝑢) ∈ 𝑟 → ((1st ‘𝑣) ∈ 𝑠 → ((1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))
120	119	exlimdv 1940	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1st ‘𝑢) ∈ 𝑟 → (∃𝑠(1st ‘𝑣) ∈ 𝑠 → ((1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))
121	120	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1st ‘𝑢) ∈ 𝑟 → ((1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) → (∃𝑠(1st ‘𝑣) ∈ 𝑠 → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))
122	121	exlimiv 1937	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑟(1st ‘𝑢) ∈ 𝑟 → ((1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) → (∃𝑠(1st ‘𝑣) ∈ 𝑠 → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))
123	94, 122	sylbi 218	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑠(1st ‘𝑢) ∈ 𝑠 → ((1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) → (∃𝑠(1st ‘𝑣) ∈ 𝑠 → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))
124	92, 123	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) → (∃𝑠(1st ‘𝑣) ∈ 𝑠 → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))
125	124	expcom 414	. . . . . . . . . . . . . . . 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 482	. . . . . . . . . . . . 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 3139	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))
131	17, 96	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ω ∈ V ∧ 𝑠 ∈ V)
132		df-goal 35577	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∀𝑔𝑖(1st ‘𝑢) = ⟨2o, ⟨𝑖, (1st ‘𝑢)⟩⟩
133		2onn 8575	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2o ∈ ω
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → 2o ∈ ω)
135		opelxpi 5662	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑖 ∈ ω ∧ (1st ‘𝑢) ∈ 𝑠) → ⟨𝑖, (1st ‘𝑢)⟩ ∈ (ω × 𝑠))
136	135	ancoms 459	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → ⟨𝑖, (1st ‘𝑢)⟩ ∈ (ω × 𝑠))
137	134, 136	opelxpd 5664	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → ⟨2o, ⟨𝑖, (1st ‘𝑢)⟩⟩ ∈ (ω × (ω × 𝑠)))
138	132, 137	eqeltrid 2844	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → ∀𝑔𝑖(1st ‘𝑢) ∈ (ω × (ω × 𝑠)))
139	138	3adant3 1138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω ∧ (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)) → ∀𝑔𝑖(1st ‘𝑢) ∈ (ω × (ω × 𝑠)))
140		eleq1 2828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢) → ((1st ‘𝑡) ∈ (ω × (ω × 𝑠)) ↔ ∀𝑔𝑖(1st ‘𝑢) ∈ (ω × (ω × 𝑠))))
141	140	3ad2ant3 1141	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω ∧ (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)) → ((1st ‘𝑡) ∈ (ω × (ω × 𝑠)) ↔ ∀𝑔𝑖(1st ‘𝑢) ∈ (ω × (ω × 𝑠))))
142	139, 141	mpbird 258	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω ∧ (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)) → (1st ‘𝑡) ∈ (ω × (ω × 𝑠)))
143		xpeq12 5650	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 = ω ∧ 𝑏 = 𝑠) → (𝑎 × 𝑏) = (ω × 𝑠))
144	143	xpeq2d 5655	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 = ω ∧ 𝑏 = 𝑠) → (ω × (𝑎 × 𝑏)) = (ω × (ω × 𝑠)))
145	144	eleq2d 2826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 = ω ∧ 𝑏 = 𝑠) → ((1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑡) ∈ (ω × (ω × 𝑠))))
146	145	spc2egv 3544	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ω ∈ V ∧ 𝑠 ∈ V) → ((1st ‘𝑡) ∈ (ω × (ω × 𝑠)) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
147	131, 142, 146	mpsyl 68	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω ∧ (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))
148	147	3exp 1125	. . . . . . . . . . . . . . . . . . 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 1937	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑠(1st ‘𝑢) ∈ 𝑠 → (𝑦 ∈ ω → ((1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢) → (𝑖 ∈ ω → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))))
152	92, 151	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑦 ∈ ω → ((1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢) → (𝑖 ∈ ω → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))))
153	152	ex 413	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑦 ∈ ω → ((1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢) → (𝑖 ∈ ω → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))))
154	153	impcomd 412	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢) → (𝑖 ∈ ω → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))))
155	154	com24 95	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → (𝑖 ∈ ω → ((1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))))
156	155	rexlimdv 3139	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → (∃𝑖 ∈ ω (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))
157	130, 156	jaod 865	. . . . . . . . . 10 ⊢ (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → ((∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))
158	157	rexlimiv 3134	. . . . . . . . 9 ⊢ (∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
159	158	adantl 482	. . . . . . . 8 ⊢ (((2nd ‘𝑡) = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢))) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
160		eqeq1 2744	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1st ‘𝑡) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ (1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
161	160	rexbidv 3164	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘𝑡) → (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ ∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
162		eqeq1 2744	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1st ‘𝑡) → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)))
163	162	rexbidv 3164	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘𝑡) → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ ∃𝑖 ∈ ω (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)))
164	161, 163	orbi12d 924	. . . . . . . . . . 11 ⊢ (𝑥 = (1st ‘𝑡) → ((∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢))))
165	164	rexbidv 3164	. . . . . . . . . 10 ⊢ (𝑥 = (1st ‘𝑡) → (∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) ↔ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢))))
166	165	anbi2d 636	. . . . . . . . 9 ⊢ (𝑥 = (1st ‘𝑡) → ((𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))) ↔ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)))))
167		eqeq1 2744	. . . . . . . . . 10 ⊢ (𝑧 = (2nd ‘𝑡) → (𝑧 = ∅ ↔ (2nd ‘𝑡) = ∅))
168	167	anbi1d 637	. . . . . . . . 9 ⊢ (𝑧 = (2nd ‘𝑡) → ((𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢))) ↔ ((2nd ‘𝑡) = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)))))
169	166, 168	elopabi 8011	. . . . . . . 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 865	. . . . . 6 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((𝑡 ∈ ((∅ Sat ∅)‘𝑦) ∨ 𝑡 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
172	72, 171	sylbid 241	. . . . 5 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
173	172	ex 413	. . . 4 ⊢ (𝑦 ∈ ω → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))
174	173	ralrimdv 3138	. . 3 ⊢ (𝑦 ∈ ω → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → ∀𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
175	75	cbvralvw 3218	. . 3 ⊢ (∀𝑤 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))
176	174, 175	imbitrrdi 253	. 2 ⊢ (𝑦 ∈ ω → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → ∀𝑤 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
177	2, 4, 6, 8, 37, 176	finds 7843	1 ⊢ (𝑁 ∈ ω → ∀𝑤 ∈ ((∅ Sat ∅)‘𝑁)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   ∧ w3a 1092   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∀wral 3054  ∃wrex 3064  Vcvv 3432   ∪ cun 3888  ∅c0 4268  ⟨cop 4568  {copab 5141   ↦ cmpt 5160   × cxp 5623  Oncon0 6317  suc csuc 6319  ‘cfv 6492  (class class class)co 7363  ωcom 7813  1^st c1st 7936  2^nd c2nd 7937  reccrdg 8345  1_oc1o 8395  2_oc2o 8396  ∈_𝑔cgoe 35568  ⊼_𝑔cgna 35569  ∀_𝑔cgol 35570   Sat csat 35571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-inf2 9560

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  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 7366  df-oprab 7367  df-mpo 7368  df-om 7814  df-1st 7938  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-1o 8402  df-2o 8403  df-map 8772  df-goel 35575  df-gona 35576  df-goal 35577  df-sat 35578

This theorem is referenced by: (None)