sat1el2xp

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)

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

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑥 = ∅ → ( ( ∅ Sat ∅ ) ‘ 𝑥 ) = ( ( ∅ Sat ∅ ) ‘ ∅ ) )
2	1	raleqdv	⊢ ( 𝑥 = ∅ → ( ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ ∅ ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
3		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( ∅ Sat ∅ ) ‘ 𝑥 ) = ( ( ∅ Sat ∅ ) ‘ 𝑦 ) )
4	3	raleqdv	⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
5		fveq2	⊢ ( 𝑥 = suc 𝑦 → ( ( ∅ Sat ∅ ) ‘ 𝑥 ) = ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) )
6	5	raleqdv	⊢ ( 𝑥 = suc 𝑦 → ( ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
7		fveq2	⊢ ( 𝑥 = 𝑁 → ( ( ∅ Sat ∅ ) ‘ 𝑥 ) = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
8	7	raleqdv	⊢ ( 𝑥 = 𝑁 → ( ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑥 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
9		eqeq1	⊢ ( 𝑥 = ( 1^st ‘ 𝑤 ) → ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ↔ ( 1^st ‘ 𝑤 ) = ( 𝑖 ∈_𝑔 𝑗 ) ) )
10	9	2rexbidv	⊢ ( 𝑥 = ( 1^st ‘ 𝑤 ) → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 1^st ‘ 𝑤 ) = ( 𝑖 ∈_𝑔 𝑗 ) ) )
11	10	anbi2d	⊢ ( 𝑥 = ( 1^st ‘ 𝑤 ) → ( ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) ↔ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 1^st ‘ 𝑤 ) = ( 𝑖 ∈_𝑔 𝑗 ) ) ) )
12		eqeq1	⊢ ( 𝑧 = ( 2^nd ‘ 𝑤 ) → ( 𝑧 = ∅ ↔ ( 2^nd ‘ 𝑤 ) = ∅ ) )
13	12	anbi1d	⊢ ( 𝑧 = ( 2^nd ‘ 𝑤 ) → ( ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 1^st ‘ 𝑤 ) = ( 𝑖 ∈_𝑔 𝑗 ) ) ↔ ( ( 2^nd ‘ 𝑤 ) = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 1^st ‘ 𝑤 ) = ( 𝑖 ∈_𝑔 𝑗 ) ) ) )
14	11 13	elopabi	⊢ ( 𝑤 ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } → ( ( 2^nd ‘ 𝑤 ) = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 1^st ‘ 𝑤 ) = ( 𝑖 ∈_𝑔 𝑗 ) ) )
15		goel	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑖 ∈_𝑔 𝑗 ) = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
16	15	eqeq2d	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ( 1^st ‘ 𝑤 ) = ( 𝑖 ∈_𝑔 𝑗 ) ↔ ( 1^st ‘ 𝑤 ) = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
17		omex	⊢ ω ∈ V
18	17 17	pm3.2i	⊢ ( ω ∈ V ∧ ω ∈ V )
19		peano1	⊢ ∅ ∈ ω
20	19	a1i	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ∅ ∈ ω )
21		opelxpi	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ω × ω ) )
22	20 21	opelxpd	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ∈ ( ω × ( ω × ω ) ) )
23		xpeq12	⊢ ( ( 𝑎 = ω ∧ 𝑏 = ω ) → ( 𝑎 × 𝑏 ) = ( ω × ω ) )
24	23	xpeq2d	⊢ ( ( 𝑎 = ω ∧ 𝑏 = ω ) → ( ω × ( 𝑎 × 𝑏 ) ) = ( ω × ( ω × ω ) ) )
25	24	eleq2d	⊢ ( ( 𝑎 = ω ∧ 𝑏 = ω ) → ( ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ∈ ( ω × ( ω × ω ) ) ) )
26	25	spc2egv	⊢ ( ( ω ∈ V ∧ ω ∈ V ) → ( ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ∈ ( ω × ( ω × ω ) ) → ∃ 𝑎 ∃ 𝑏 ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
27	18 22 26	mpsyl	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ∃ 𝑎 ∃ 𝑏 ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ∈ ( ω × ( 𝑎 × 𝑏 ) ) )
28		eleq1	⊢ ( ( 1^st ‘ 𝑤 ) = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → ( ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
29	28	2exbidv	⊢ ( ( 1^st ‘ 𝑤 ) = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → ( ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ∃ 𝑎 ∃ 𝑏 ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
30	27 29	syl5ibrcom	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ( 1^st ‘ 𝑤 ) = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
31	16 30	sylbid	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( ( 1^st ‘ 𝑤 ) = ( 𝑖 ∈_𝑔 𝑗 ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
32	31	rexlimivv	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 1^st ‘ 𝑤 ) = ( 𝑖 ∈_𝑔 𝑗 ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) )
33	32	adantl	⊢ ( ( ( 2^nd ‘ 𝑤 ) = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 1^st ‘ 𝑤 ) = ( 𝑖 ∈_𝑔 𝑗 ) ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) )
34	14 33	syl	⊢ ( 𝑤 ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) )
35		satf00	⊢ ( ( ∅ Sat ∅ ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) }
36	34 35	eleq2s	⊢ ( 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ ∅ ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) )
37	36	rgen	⊢ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ ∅ ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) )
38		omsucelsucb	⊢ ( 𝑦 ∈ ω ↔ suc 𝑦 ∈ suc ω )
39		satf0sucom	⊢ ( suc 𝑦 ∈ suc ω → ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ suc 𝑦 ) )
40	38 39	sylbi	⊢ ( 𝑦 ∈ ω → ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ suc 𝑦 ) )
41	40	adantr	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ suc 𝑦 ) )
42		nnon	⊢ ( 𝑦 ∈ ω → 𝑦 ∈ On )
43		rdgsuc	⊢ ( 𝑦 ∈ On → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ suc 𝑦 ) = ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑦 ) ) )
44	42 43	syl	⊢ ( 𝑦 ∈ ω → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ suc 𝑦 ) = ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑦 ) ) )
45	44	adantr	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ suc 𝑦 ) = ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑦 ) ) )
46		elelsuc	⊢ ( 𝑦 ∈ ω → 𝑦 ∈ suc ω )
47		satf0sucom	⊢ ( 𝑦 ∈ suc ω → ( ( ∅ Sat ∅ ) ‘ 𝑦 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑦 ) )
48	46 47	syl	⊢ ( 𝑦 ∈ ω → ( ( ∅ Sat ∅ ) ‘ 𝑦 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑦 ) )
49	48	eqcomd	⊢ ( 𝑦 ∈ ω → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑦 ) = ( ( ∅ Sat ∅ ) ‘ 𝑦 ) )
50	49	fveq2d	⊢ ( 𝑦 ∈ ω → ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑦 ) ) = ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) )
51	50	adantr	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑦 ) ) = ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) )
52		eqidd	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) = ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) )
53		id	⊢ ( 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑦 ) )
54		rexeq	⊢ ( 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ↔ ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
55	54	orbi1d	⊢ ( 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ↔ ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
56	55	rexeqbi1dv	⊢ ( 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ↔ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
57	56	anbi2d	⊢ ( 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ↔ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ) )
58	57	opabbidv	⊢ ( 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } )
59	53 58	uneq12d	⊢ ( 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) = ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
60	59	adantl	⊢ ( ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ∧ 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) → ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) = ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
61		fvexd	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∈ V )
62	17	a1i	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ω ∈ V )
63		satf0suclem	⊢ ( ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∈ V ∧ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∈ V ∧ ω ∈ V ) → { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ∈ V )
64	61 61 62 63	syl3anc	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ∈ V )
65		unexg	⊢ ( ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∈ V ∧ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ∈ V ) → ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ∈ V )
66	61 64 65	syl2anc	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ∈ V )
67	52 60 61 66	fvmptd	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ) = ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
68	45 51 67	3eqtrd	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ suc 𝑦 ) = ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
69	41 68	eqtrd	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) = ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
70	69	eleq2d	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( 𝑡 ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ↔ 𝑡 ∈ ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) )
71		elun	⊢ ( 𝑡 ∈ ( ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∪ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ↔ ( 𝑡 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∨ 𝑡 ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
72	70 71	bitrdi	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( 𝑡 ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ↔ ( 𝑡 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∨ 𝑡 ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) )
73		fveq2	⊢ ( 𝑤 = 𝑡 → ( 1^st ‘ 𝑤 ) = ( 1^st ‘ 𝑡 ) )
74	73	eleq1d	⊢ ( 𝑤 = 𝑡 → ( ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
75	74	2exbidv	⊢ ( 𝑤 = 𝑡 → ( ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
76	75	rspccv	⊢ ( ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) → ( 𝑡 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
77	76	adantl	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( 𝑡 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
78		fveq2	⊢ ( 𝑤 = 𝑣 → ( 1^st ‘ 𝑤 ) = ( 1^st ‘ 𝑣 ) )
79	78	eleq1d	⊢ ( 𝑤 = 𝑣 → ( ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ( 1^st ‘ 𝑣 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
80	79	2exbidv	⊢ ( 𝑤 = 𝑣 → ( ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑣 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
81	80	rspcva	⊢ ( ( 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑣 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) )
82		sels	⊢ ( ( 1^st ‘ 𝑣 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) → ∃ 𝑠 ( 1^st ‘ 𝑣 ) ∈ 𝑠 )
83	82	exlimivv	⊢ ( ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑣 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) → ∃ 𝑠 ( 1^st ‘ 𝑣 ) ∈ 𝑠 )
84	81 83	syl	⊢ ( ( 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ∃ 𝑠 ( 1^st ‘ 𝑣 ) ∈ 𝑠 )
85	84	expcom	⊢ ( ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) → ( 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ∃ 𝑠 ( 1^st ‘ 𝑣 ) ∈ 𝑠 ) )
86		fveq2	⊢ ( 𝑤 = 𝑢 → ( 1^st ‘ 𝑤 ) = ( 1^st ‘ 𝑢 ) )
87	86	eleq1d	⊢ ( 𝑤 = 𝑢 → ( ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ( 1^st ‘ 𝑢 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
88	87	2exbidv	⊢ ( 𝑤 = 𝑢 → ( ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑢 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
89	88	rspcva	⊢ ( ( 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑢 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) )
90		sels	⊢ ( ( 1^st ‘ 𝑢 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) → ∃ 𝑠 ( 1^st ‘ 𝑢 ) ∈ 𝑠 )
91	90	exlimivv	⊢ ( ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑢 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) → ∃ 𝑠 ( 1^st ‘ 𝑢 ) ∈ 𝑠 )
92	89 91	syl	⊢ ( ( 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ∃ 𝑠 ( 1^st ‘ 𝑢 ) ∈ 𝑠 )
93		eleq2w	⊢ ( 𝑠 = 𝑟 → ( ( 1^st ‘ 𝑢 ) ∈ 𝑠 ↔ ( 1^st ‘ 𝑢 ) ∈ 𝑟 ) )
94	93	cbvexvw	⊢ ( ∃ 𝑠 ( 1^st ‘ 𝑢 ) ∈ 𝑠 ↔ ∃ 𝑟 ( 1^st ‘ 𝑢 ) ∈ 𝑟 )
95		vex	⊢ 𝑟 ∈ V
96		vex	⊢ 𝑠 ∈ V
97	95 96	pm3.2i	⊢ ( 𝑟 ∈ V ∧ 𝑠 ∈ V )
98		df-ov	⊢ ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ( ⊼_𝑔 ‘ ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ )
99		df-gona	⊢ ⊼_𝑔 = ( 𝑒 ∈ ( V × V ) ↦ ⟨ 1_o , 𝑒 ⟩ )
100		opeq2	⊢ ( 𝑒 = ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ → ⟨ 1_o , 𝑒 ⟩ = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ )
101		opelvvg	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑟 ∧ ( 1^st ‘ 𝑣 ) ∈ 𝑠 ) → ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ∈ ( V × V ) )
102		opex	⊢ ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ ∈ V
103	102	a1i	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑟 ∧ ( 1^st ‘ 𝑣 ) ∈ 𝑠 ) → ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ ∈ V )
104	99 100 101 103	fvmptd3	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑟 ∧ ( 1^st ‘ 𝑣 ) ∈ 𝑠 ) → ( ⊼_𝑔 ‘ ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ) = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ )
105	98 104	eqtrid	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑟 ∧ ( 1^st ‘ 𝑣 ) ∈ 𝑠 ) → ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ )
106		1onn	⊢ 1_o ∈ ω
107	106	a1i	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑟 ∧ ( 1^st ‘ 𝑣 ) ∈ 𝑠 ) → 1_o ∈ ω )
108		opelxpi	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑟 ∧ ( 1^st ‘ 𝑣 ) ∈ 𝑠 ) → ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ∈ ( 𝑟 × 𝑠 ) )
109	107 108	opelxpd	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑟 ∧ ( 1^st ‘ 𝑣 ) ∈ 𝑠 ) → ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ ∈ ( ω × ( 𝑟 × 𝑠 ) ) )
110	105 109	eqeltrd	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑟 ∧ ( 1^st ‘ 𝑣 ) ∈ 𝑠 ) → ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∈ ( ω × ( 𝑟 × 𝑠 ) ) )
111		xpeq12	⊢ ( ( 𝑎 = 𝑟 ∧ 𝑏 = 𝑠 ) → ( 𝑎 × 𝑏 ) = ( 𝑟 × 𝑠 ) )
112	111	xpeq2d	⊢ ( ( 𝑎 = 𝑟 ∧ 𝑏 = 𝑠 ) → ( ω × ( 𝑎 × 𝑏 ) ) = ( ω × ( 𝑟 × 𝑠 ) ) )
113	112	eleq2d	⊢ ( ( 𝑎 = 𝑟 ∧ 𝑏 = 𝑠 ) → ( ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∈ ( ω × ( 𝑟 × 𝑠 ) ) ) )
114	113	spc2egv	⊢ ( ( 𝑟 ∈ V ∧ 𝑠 ∈ V ) → ( ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∈ ( ω × ( 𝑟 × 𝑠 ) ) → ∃ 𝑎 ∃ 𝑏 ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
115	97 110 114	mpsyl	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑟 ∧ ( 1^st ‘ 𝑣 ) ∈ 𝑠 ) → ∃ 𝑎 ∃ 𝑏 ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) )
116		eleq1	⊢ ( ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
117	116	2exbidv	⊢ ( ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ∃ 𝑎 ∃ 𝑏 ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
118	115 117	syl5ibrcom	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑟 ∧ ( 1^st ‘ 𝑣 ) ∈ 𝑠 ) → ( ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
119	118	ex	⊢ ( ( 1^st ‘ 𝑢 ) ∈ 𝑟 → ( ( 1^st ‘ 𝑣 ) ∈ 𝑠 → ( ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) )
120	119	exlimdv	⊢ ( ( 1^st ‘ 𝑢 ) ∈ 𝑟 → ( ∃ 𝑠 ( 1^st ‘ 𝑣 ) ∈ 𝑠 → ( ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) )
121	120	com23	⊢ ( ( 1^st ‘ 𝑢 ) ∈ 𝑟 → ( ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( ∃ 𝑠 ( 1^st ‘ 𝑣 ) ∈ 𝑠 → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) )
122	121	exlimiv	⊢ ( ∃ 𝑟 ( 1^st ‘ 𝑢 ) ∈ 𝑟 → ( ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( ∃ 𝑠 ( 1^st ‘ 𝑣 ) ∈ 𝑠 → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) )
123	94 122	sylbi	⊢ ( ∃ 𝑠 ( 1^st ‘ 𝑢 ) ∈ 𝑠 → ( ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( ∃ 𝑠 ( 1^st ‘ 𝑣 ) ∈ 𝑠 → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) )
124	92 123	syl	⊢ ( ( 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( ∃ 𝑠 ( 1^st ‘ 𝑣 ) ∈ 𝑠 → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) )
125	124	expcom	⊢ ( ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) → ( 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( ∃ 𝑠 ( 1^st ‘ 𝑣 ) ∈ 𝑠 → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) ) )
126	125	com24	⊢ ( ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) → ( ∃ 𝑠 ( 1^st ‘ 𝑣 ) ∈ 𝑠 → ( ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) ) )
127	85 126	syld	⊢ ( ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) → ( 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) ) )
128	127	adantl	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) ) )
129	128	com14	⊢ ( 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) ) )
130	129	rexlimdv	⊢ ( 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) )
131	17 96	pm3.2i	⊢ ( ω ∈ V ∧ 𝑠 ∈ V )
132		df-goal	⊢ ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ⟨ 2_o , ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ⟩
133		2onn	⊢ 2_o ∈ ω
134	133	a1i	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑠 ∧ 𝑖 ∈ ω ) → 2_o ∈ ω )
135		opelxpi	⊢ ( ( 𝑖 ∈ ω ∧ ( 1^st ‘ 𝑢 ) ∈ 𝑠 ) → ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ∈ ( ω × 𝑠 ) )
136	135	ancoms	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑠 ∧ 𝑖 ∈ ω ) → ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ∈ ( ω × 𝑠 ) )
137	134 136	opelxpd	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑠 ∧ 𝑖 ∈ ω ) → ⟨ 2_o , ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ⟩ ∈ ( ω × ( ω × 𝑠 ) ) )
138	132 137	eqeltrid	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑠 ∧ 𝑖 ∈ ω ) → ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∈ ( ω × ( ω × 𝑠 ) ) )
139	138	3adant3	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑠 ∧ 𝑖 ∈ ω ∧ ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∈ ( ω × ( ω × 𝑠 ) ) )
140		eleq1	⊢ ( ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( ( 1^st ‘ 𝑡 ) ∈ ( ω × ( ω × 𝑠 ) ) ↔ ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∈ ( ω × ( ω × 𝑠 ) ) ) )
141	140	3ad2ant3	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑠 ∧ 𝑖 ∈ ω ∧ ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ( ( 1^st ‘ 𝑡 ) ∈ ( ω × ( ω × 𝑠 ) ) ↔ ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∈ ( ω × ( ω × 𝑠 ) ) ) )
142	139 141	mpbird	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑠 ∧ 𝑖 ∈ ω ∧ ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ( 1^st ‘ 𝑡 ) ∈ ( ω × ( ω × 𝑠 ) ) )
143		xpeq12	⊢ ( ( 𝑎 = ω ∧ 𝑏 = 𝑠 ) → ( 𝑎 × 𝑏 ) = ( ω × 𝑠 ) )
144	143	xpeq2d	⊢ ( ( 𝑎 = ω ∧ 𝑏 = 𝑠 ) → ( ω × ( 𝑎 × 𝑏 ) ) = ( ω × ( ω × 𝑠 ) ) )
145	144	eleq2d	⊢ ( ( 𝑎 = ω ∧ 𝑏 = 𝑠 ) → ( ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ( 1^st ‘ 𝑡 ) ∈ ( ω × ( ω × 𝑠 ) ) ) )
146	145	spc2egv	⊢ ( ( ω ∈ V ∧ 𝑠 ∈ V ) → ( ( 1^st ‘ 𝑡 ) ∈ ( ω × ( ω × 𝑠 ) ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
147	131 142 146	mpsyl	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ 𝑠 ∧ 𝑖 ∈ ω ∧ ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) )
148	147	3exp	⊢ ( ( 1^st ‘ 𝑢 ) ∈ 𝑠 → ( 𝑖 ∈ ω → ( ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) )
149	148	com23	⊢ ( ( 1^st ‘ 𝑢 ) ∈ 𝑠 → ( ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( 𝑖 ∈ ω → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) )
150	149	a1d	⊢ ( ( 1^st ‘ 𝑢 ) ∈ 𝑠 → ( 𝑦 ∈ ω → ( ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( 𝑖 ∈ ω → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) ) )
151	150	exlimiv	⊢ ( ∃ 𝑠 ( 1^st ‘ 𝑢 ) ∈ 𝑠 → ( 𝑦 ∈ ω → ( ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( 𝑖 ∈ ω → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) ) )
152	92 151	syl	⊢ ( ( 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( 𝑦 ∈ ω → ( ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( 𝑖 ∈ ω → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) ) )
153	152	ex	⊢ ( 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) → ( 𝑦 ∈ ω → ( ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( 𝑖 ∈ ω → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) ) ) )
154	153	impcomd	⊢ ( 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( 𝑖 ∈ ω → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) ) )
155	154	com24	⊢ ( 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( 𝑖 ∈ ω → ( ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) ) )
156	155	rexlimdv	⊢ ( 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( ∃ 𝑖 ∈ ω ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) )
157	130 156	jaod	⊢ ( 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) → ( ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) )
158	157	rexlimiv	⊢ ( ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
159	158	adantl	⊢ ( ( ( 2^nd ‘ 𝑡 ) = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) → ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
160		eqeq1	⊢ ( 𝑥 = ( 1^st ‘ 𝑡 ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ↔ ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
161	160	rexbidv	⊢ ( 𝑥 = ( 1^st ‘ 𝑡 ) → ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ↔ ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
162		eqeq1	⊢ ( 𝑥 = ( 1^st ‘ 𝑡 ) → ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ↔ ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) )
163	162	rexbidv	⊢ ( 𝑥 = ( 1^st ‘ 𝑡 ) → ( ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ↔ ∃ 𝑖 ∈ ω ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) )
164	161 163	orbi12d	⊢ ( 𝑥 = ( 1^st ‘ 𝑡 ) → ( ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ↔ ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
165	164	rexbidv	⊢ ( 𝑥 = ( 1^st ‘ 𝑡 ) → ( ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ↔ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
166	165	anbi2d	⊢ ( 𝑥 = ( 1^st ‘ 𝑡 ) → ( ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ↔ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ) )
167		eqeq1	⊢ ( 𝑧 = ( 2^nd ‘ 𝑡 ) → ( 𝑧 = ∅ ↔ ( 2^nd ‘ 𝑡 ) = ∅ ) )
168	167	anbi1d	⊢ ( 𝑧 = ( 2^nd ‘ 𝑡 ) → ( ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ↔ ( ( 2^nd ‘ 𝑡 ) = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ) )
169	166 168	elopabi	⊢ ( 𝑡 ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } → ( ( 2^nd ‘ 𝑡 ) = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( 1^st ‘ 𝑡 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω ( 1^st ‘ 𝑡 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
170	159 169	syl11	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( 𝑡 ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
171	77 170	jaod	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( ( 𝑡 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∨ 𝑡 ∈ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
172	72 171	sylbid	⊢ ( ( 𝑦 ∈ ω ∧ ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) → ( 𝑡 ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
173	172	ex	⊢ ( 𝑦 ∈ ω → ( ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) → ( 𝑡 ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) → ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) ) )
174	173	ralrimdv	⊢ ( 𝑦 ∈ ω → ( ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) → ∀ 𝑡 ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
175	75	cbvralvw	⊢ ( ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ↔ ∀ 𝑡 ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑡 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) )
176	174 175	imbitrrdi	⊢ ( 𝑦 ∈ ω → ( ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) → ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ suc 𝑦 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) ) )
177	2 4 6 8 37 176	finds	⊢ ( 𝑁 ∈ ω → ∀ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∃ 𝑎 ∃ 𝑏 ( 1^st ‘ 𝑤 ) ∈ ( ω × ( 𝑎 × 𝑏 ) ) )

Metamath Proof Explorer

Theorem sat1el2xp

Proof