Theorem sat1el2xp 35444

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 6828	. . 3 ⊢ (𝑥 = ∅ → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘∅))
2	1	raleqdv 3293	. 2 ⊢ (𝑥 = ∅ → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘∅)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
3		fveq2 6828	. . 3 ⊢ (𝑥 = 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘𝑦))
4	3	raleqdv 3293	. 2 ⊢ (𝑥 = 𝑦 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
5		fveq2 6828	. . 3 ⊢ (𝑥 = suc 𝑦 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘suc 𝑦))
6	5	raleqdv 3293	. 2 ⊢ (𝑥 = suc 𝑦 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
7		fveq2 6828	. . 3 ⊢ (𝑥 = 𝑁 → ((∅ Sat ∅)‘𝑥) = ((∅ Sat ∅)‘𝑁))
8	7	raleqdv 3293	. 2 ⊢ (𝑥 = 𝑁 → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑥)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑁)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))))
9		eqeq1 2737	. . . . . . . 8 ⊢ (𝑥 = (1st ‘𝑤) → (𝑥 = (𝑖∈𝑔𝑗) ↔ (1st ‘𝑤) = (𝑖∈𝑔𝑗)))
10	9	2rexbidv 3198	. . . . . . 7 ⊢ (𝑥 = (1st ‘𝑤) → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)))
11	10	anbi2d 630	. . . . . 6 ⊢ (𝑥 = (1st ‘𝑤) → ((𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) ↔ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗))))
12		eqeq1 2737	. . . . . . 7 ⊢ (𝑧 = (2nd ‘𝑤) → (𝑧 = ∅ ↔ (2nd ‘𝑤) = ∅))
13	12	anbi1d 631	. . . . . 6 ⊢ (𝑧 = (2nd ‘𝑤) → ((𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)) ↔ ((2nd ‘𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗))))
14	11, 13	elopabi 8000	. . . . 5 ⊢ (𝑤 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} → ((2nd ‘𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)))
15		goel 35412	. . . . . . . . 9 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖∈𝑔𝑗) = ⟨∅, ⟨𝑖, 𝑗⟩⟩)
16	15	eqeq2d 2744	. . . . . . . 8 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((1st ‘𝑤) = (𝑖∈𝑔𝑗) ↔ (1st ‘𝑤) = ⟨∅, ⟨𝑖, 𝑗⟩⟩))
17		omex 9540	. . . . . . . . . . 11 ⊢ ω ∈ V
18	17, 17	pm3.2i 470	. . . . . . . . . 10 ⊢ (ω ∈ V ∧ ω ∈ V)
19		peano1 7825	. . . . . . . . . . . 12 ⊢ ∅ ∈ ω
20	19	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ∅ ∈ ω)
21		opelxpi 5656	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ⟨𝑖, 𝑗⟩ ∈ (ω × ω))
22	20, 21	opelxpd 5658	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (ω × ω)))
23		xpeq12 5644	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ω ∧ 𝑏 = ω) → (𝑎 × 𝑏) = (ω × ω))
24	23	xpeq2d 5649	. . . . . . . . . . . 12 ⊢ ((𝑎 = ω ∧ 𝑏 = ω) → (ω × (𝑎 × 𝑏)) = (ω × (ω × ω)))
25	24	eleq2d 2819	. . . . . . . . . . 11 ⊢ ((𝑎 = ω ∧ 𝑏 = ω) → (⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏)) ↔ ⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (ω × ω))))
26	25	spc2egv 3550	. . . . . . . . . 10 ⊢ ((ω ∈ V ∧ ω ∈ V) → (⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (ω × ω)) → ∃𝑎∃𝑏⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏))))
27	18, 22, 26	mpsyl 68	. . . . . . . . 9 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ∃𝑎∃𝑏⟨∅, ⟨𝑖, 𝑗⟩⟩ ∈ (ω × (𝑎 × 𝑏)))
28		eleq1 2821	. . . . . . . . . 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 3175	. . . . . 6 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
33	32	adantl 481	. . . . 5 ⊢ (((2nd ‘𝑤) = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (1st ‘𝑤) = (𝑖∈𝑔𝑗)) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
34	14, 33	syl 17	. . . 4 ⊢ (𝑤 ∈ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
35		satf00 35439	. . . 4 ⊢ ((∅ Sat ∅)‘∅) = {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))}
36	34, 35	eleq2s 2851	. . 3 ⊢ (𝑤 ∈ ((∅ Sat ∅)‘∅) → ∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))
37	36	rgen 3050	. 2 ⊢ ∀𝑤 ∈ ((∅ Sat ∅)‘∅)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))
38		omsucelsucb 8383	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈ suc ω)
39		satf0sucom 35438	. . . . . . . . . . 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 7808	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ω → 𝑦 ∈ On)
43		rdgsuc 8349	. . . . . . . . . . . 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 6386	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ω → 𝑦 ∈ suc ω)
47		satf0sucom 35438	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ suc ω → ((∅ Sat ∅)‘𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦))
48	46, 47	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ω → ((∅ Sat ∅)‘𝑦) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦))
49	48	eqcomd 2739	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ω → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘𝑦) = ((∅ Sat ∅)‘𝑦))
50	49	fveq2d 6832	. . . . . . . . . . 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 2734	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})) = (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})))
53		id 22	. . . . . . . . . . . . 13 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → 𝑓 = ((∅ Sat ∅)‘𝑦))
54		rexeq 3289	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ ∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
55	54	orbi1d 916	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → ((∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))
56	55	rexeqbi1dv 3306	. . . . . . . . . . . . . . 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 5159	. . . . . . . . . . . . 13 ⊢ (𝑓 = ((∅ Sat ∅)‘𝑦) → {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))} = {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})
59	53, 58	uneq12d 4118	. . . . . . . . . . . 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 6843	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((∅ Sat ∅)‘𝑦) ∈ V)
62	17	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ω ∈ V)
63		satf0suclem 35440	. . . . . . . . . . . . 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 7682	. . . . . . . . . . . 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 6942	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))‘((∅ Sat ∅)‘𝑦)) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))
68	45, 51, 67	3eqtrd 2772	. . . . . . . . 9 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})), {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})‘suc 𝑦) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))
69	41, 68	eqtrd 2768	. . . . . . . 8 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ((∅ Sat ∅)‘suc 𝑦) = (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))}))
70	69	eleq2d 2819	. . . . . . 7 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦) ↔ 𝑡 ∈ (((∅ Sat ∅)‘𝑦) ∪ {⟨𝑥, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑢 ∈ ((∅ Sat ∅)‘𝑦)(∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))})))
71		elun 4102	. . . . . . 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 6828	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑡 → (1st ‘𝑤) = (1st ‘𝑡))
74	73	eleq1d 2818	. . . . . . . . . 10 ⊢ (𝑤 = 𝑡 → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
75	74	2exbidv 1925	. . . . . . . . 9 ⊢ (𝑤 = 𝑡 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
76	75	rspccv 3570	. . . . . . . 8 ⊢ (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → (𝑡 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
77	76	adantl 481	. . . . . . 7 ⊢ ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → (𝑡 ∈ ((∅ Sat ∅)‘𝑦) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
78		fveq2 6828	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑣 → (1st ‘𝑤) = (1st ‘𝑣))
79	78	eleq1d 2818	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑣 → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏))))
80	79	2exbidv 1925	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑣 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏(1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏))))
81	80	rspcva 3571	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑣) ∈ (ω × (𝑎 × 𝑏)))
82		sels 5383	. . . . . . . . . . . . . . . . . 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 6828	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑢 → (1st ‘𝑤) = (1st ‘𝑢))
87	86	eleq1d 2818	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑢 → ((1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏))))
88	87	2exbidv 1925	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑢 → (∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) ↔ ∃𝑎∃𝑏(1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏))))
89	88	rspcva 3571	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)))
90		sels 5383	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑢) ∈ 𝑠)
91	90	exlimivv 1933	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑎∃𝑏(1st ‘𝑢) ∈ (ω × (𝑎 × 𝑏)) → ∃𝑠(1st ‘𝑢) ∈ 𝑠)
92	89, 91	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ ((∅ Sat ∅)‘𝑦) ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑠(1st ‘𝑢) ∈ 𝑠)
93		eleq2w 2817	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 = 𝑟 → ((1st ‘𝑢) ∈ 𝑠 ↔ (1st ‘𝑢) ∈ 𝑟))
94	93	cbvexvw 2038	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑠(1st ‘𝑢) ∈ 𝑠 ↔ ∃𝑟(1st ‘𝑢) ∈ 𝑟)
95		vex 3441	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑟 ∈ V
96		vex 3441	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑠 ∈ V
97	95, 96	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑟 ∈ V ∧ 𝑠 ∈ V)
98		df-ov 7355	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) = (⊼𝑔‘⟨(1st ‘𝑢), (1st ‘𝑣)⟩)
99		df-gona 35406	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ⊼𝑔 = (𝑒 ∈ (V × V) ↦ ⟨1o, 𝑒⟩)
100		opeq2 4825	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑒 = ⟨(1st ‘𝑢), (1st ‘𝑣)⟩ → ⟨1o, 𝑒⟩ = ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩)
101		opelvvg 5660	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨(1st ‘𝑢), (1st ‘𝑣)⟩ ∈ (V × V))
102		opex 5407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩ ∈ V
103	102	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩ ∈ V)
104	99, 100, 101, 103	fvmptd3 6958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → (⊼𝑔‘⟨(1st ‘𝑢), (1st ‘𝑣)⟩) = ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩)
105	98, 104	eqtrid 2780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) = ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩)
106		1onn 8561	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 1o ∈ ω
107	106	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → 1o ∈ ω)
108		opelxpi 5656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨(1st ‘𝑢), (1st ‘𝑣)⟩ ∈ (𝑟 × 𝑠))
109	107, 108	opelxpd 5658	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ⟨1o, ⟨(1st ‘𝑢), (1st ‘𝑣)⟩⟩ ∈ (ω × (𝑟 × 𝑠)))
110	105, 109	eqeltrd 2833	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑟 × 𝑠)))
111		xpeq12 5644	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 = 𝑟 ∧ 𝑏 = 𝑠) → (𝑎 × 𝑏) = (𝑟 × 𝑠))
112	111	xpeq2d 5649	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 = 𝑟 ∧ 𝑏 = 𝑠) → (ω × (𝑎 × 𝑏)) = (ω × (𝑟 × 𝑠)))
113	112	eleq2d 2819	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 = 𝑟 ∧ 𝑏 = 𝑠) → (((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑎 × 𝑏)) ↔ ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑟 × 𝑠))))
114	113	spc2egv 3550	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑟 ∈ V ∧ 𝑠 ∈ V) → (((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑟 × 𝑠)) → ∃𝑎∃𝑏((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑎 × 𝑏))))
115	97, 110, 114	mpsyl 68	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1st ‘𝑢) ∈ 𝑟 ∧ (1st ‘𝑣) ∈ 𝑠) → ∃𝑎∃𝑏((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∈ (ω × (𝑎 × 𝑏)))
116		eleq1 2821	. . . . . . . . . . . . . . . . . . . . . . . . 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 3132	. . . . . . . . . . 11 ⊢ (𝑢 ∈ ((∅ Sat ∅)‘𝑦) → (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) → ((𝑦 ∈ ω ∧ ∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏))) → ∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)))))
131	17, 96	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ω ∈ V ∧ 𝑠 ∈ V)
132		df-goal 35407	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∀𝑔𝑖(1st ‘𝑢) = ⟨2o, ⟨𝑖, (1st ‘𝑢)⟩⟩
133		2onn 8563	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 2o ∈ ω
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → 2o ∈ ω)
135		opelxpi 5656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑖 ∈ ω ∧ (1st ‘𝑢) ∈ 𝑠) → ⟨𝑖, (1st ‘𝑢)⟩ ∈ (ω × 𝑠))
136	135	ancoms 458	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → ⟨𝑖, (1st ‘𝑢)⟩ ∈ (ω × 𝑠))
137	134, 136	opelxpd 5658	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → ⟨2o, ⟨𝑖, (1st ‘𝑢)⟩⟩ ∈ (ω × (ω × 𝑠)))
138	132, 137	eqeltrid 2837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω) → ∀𝑔𝑖(1st ‘𝑢) ∈ (ω × (ω × 𝑠)))
139	138	3adant3 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1st ‘𝑢) ∈ 𝑠 ∧ 𝑖 ∈ ω ∧ (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)) → ∀𝑔𝑖(1st ‘𝑢) ∈ (ω × (ω × 𝑠)))
140		eleq1 2821	. . . . . . . . . . . . . . . . . . . . . . 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 5644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 = ω ∧ 𝑏 = 𝑠) → (𝑎 × 𝑏) = (ω × 𝑠))
144	143	xpeq2d 5649	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 = ω ∧ 𝑏 = 𝑠) → (ω × (𝑎 × 𝑏)) = (ω × (ω × 𝑠)))
145	144	eleq2d 2819	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 = ω ∧ 𝑏 = 𝑠) → ((1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏)) ↔ (1st ‘𝑡) ∈ (ω × (ω × 𝑠))))
146	145	spc2egv 3550	. . . . . . . . . . . . . . . . . . . . 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 3132	. . . . . . . . . . 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 3127	. . . . . . . . 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 2737	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1st ‘𝑡) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ (1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
161	160	rexbidv 3157	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘𝑡) → (∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ ∃𝑣 ∈ ((∅ Sat ∅)‘𝑦)(1st ‘𝑡) = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
162		eqeq1 2737	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1st ‘𝑡) → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ (1st ‘𝑡) = ∀𝑔𝑖(1st ‘𝑢)))
163	162	rexbidv 3157	. . . . . . . . . . . 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 3157	. . . . . . . . . 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 2737	. . . . . . . . . 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 8000	. . . . . . . 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 3131	. . 3 ⊢ (𝑦 ∈ ω → (∀𝑤 ∈ ((∅ Sat ∅)‘𝑦)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)) → ∀𝑡 ∈ ((∅ Sat ∅)‘suc 𝑦)∃𝑎∃𝑏(1st ‘𝑡) ∈ (ω × (𝑎 × 𝑏))))
175	75	cbvralvw 3211	. . 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 7832	1 ⊢ (𝑁 ∈ ω → ∀𝑤 ∈ ((∅ Sat ∅)‘𝑁)∃𝑎∃𝑏(1st ‘𝑤) ∈ (ω × (𝑎 × 𝑏)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∀wral 3048  ∃wrex 3057  Vcvv 3437   ∪ cun 3896  ∅c0 4282  ⟨cop 4581  {copab 5155   ↦ cmpt 5174   × cxp 5617  Oncon0 6311  suc csuc 6313  ‘cfv 6486  (class class class)co 7352  ωcom 7802  1^st c1st 7925  2^nd c2nd 7926  reccrdg 8334  1_oc1o 8384  2_oc2o 8385  ∈_𝑔cgoe 35398  ⊼_𝑔cgna 35399  ∀_𝑔cgol 35400   Sat csat 35401

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 2182  ax-ext 2705  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-inf2 9538

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357  df-om 7803  df-1st 7927  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-1o 8391  df-2o 8392  df-map 8758  df-goel 35405  df-gona 35406  df-goal 35407  df-sat 35408

This theorem is referenced by: (None)