fmlasuc0

Description: The valid Godel formulas of height ( N + 1 ) . (Contributed by AV, 18-Sep-2023)

		Ref	Expression
	Assertion	fmlasuc0	⊢ ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		df-fmla	⊢ Fmla = ( 𝑛 ∈ suc ω ↦ dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) )
2		fveq2	⊢ ( 𝑛 = suc 𝑁 → ( ( ∅ Sat ∅ ) ‘ 𝑛 ) = ( ( ∅ Sat ∅ ) ‘ suc 𝑁 ) )
3	2	dmeqd	⊢ ( 𝑛 = suc 𝑁 → dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) = dom ( ( ∅ Sat ∅ ) ‘ suc 𝑁 ) )
4		omsucelsucb	⊢ ( 𝑁 ∈ ω ↔ suc 𝑁 ∈ suc ω )
5	4	biimpi	⊢ ( 𝑁 ∈ ω → suc 𝑁 ∈ suc ω )
6		fvex	⊢ ( ( ∅ Sat ∅ ) ‘ suc 𝑁 ) ∈ V
7	6	dmex	⊢ dom ( ( ∅ Sat ∅ ) ‘ suc 𝑁 ) ∈ V
8	7	a1i	⊢ ( 𝑁 ∈ ω → dom ( ( ∅ Sat ∅ ) ‘ suc 𝑁 ) ∈ V )
9	1 3 5 8	fvmptd3	⊢ ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ suc 𝑁 ) )
10		satf0sucom	⊢ ( suc 𝑁 ∈ suc ω → ( ( ∅ Sat ∅ ) ‘ suc 𝑁 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ suc 𝑁 ) )
11	5 10	syl	⊢ ( 𝑁 ∈ ω → ( ( ∅ Sat ∅ ) ‘ suc 𝑁 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ suc 𝑁 ) )
12		nnon	⊢ ( 𝑁 ∈ ω → 𝑁 ∈ On )
13		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 ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) ) )
14	12 13	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 ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) ) )
15	11 14	eqtrd	⊢ ( 𝑁 ∈ ω → ( ( ∅ Sat ∅ ) ‘ suc 𝑁 ) = ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) ) )
16	15	dmeqd	⊢ ( 𝑁 ∈ ω → dom ( ( ∅ Sat ∅ ) ‘ suc 𝑁 ) = dom ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) ) )
17		elelsuc	⊢ ( 𝑁 ∈ ω → 𝑁 ∈ suc ω )
18		satf0sucom	⊢ ( 𝑁 ∈ suc ω → ( ( ∅ Sat ∅ ) ‘ 𝑁 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) )
19	18	eqcomd	⊢ ( 𝑁 ∈ suc ω → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
20	17 19	syl	⊢ ( 𝑁 ∈ ω → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
21	20	fveq2d	⊢ ( 𝑁 ∈ ω → ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) ) = ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
22		eqidd	⊢ ( 𝑁 ∈ ω → ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) = ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) )
23		id	⊢ ( 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
24		rexeq	⊢ ( 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ↔ ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
25	24	orbi1d	⊢ ( 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ↔ ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
26	25	rexeqbi1dv	⊢ ( 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → ( ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ↔ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
27	26	anbi2d	⊢ ( 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → ( ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ↔ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ) )
28	27	opabbidv	⊢ ( 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } )
29	23 28	uneq12d	⊢ ( 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) = ( ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
30	29	adantl	⊢ ( ( 𝑁 ∈ ω ∧ 𝑓 = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) = ( ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
31		fvex	⊢ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∈ V
32	31	a1i	⊢ ( 𝑁 ∈ ω → ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∈ V )
33		peano1	⊢ ∅ ∈ ω
34		eleq1	⊢ ( 𝑦 = ∅ → ( 𝑦 ∈ ω ↔ ∅ ∈ ω ) )
35	33 34	mpbiri	⊢ ( 𝑦 = ∅ → 𝑦 ∈ ω )
36	35	adantr	⊢ ( ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) → 𝑦 ∈ ω )
37	36	pm4.71ri	⊢ ( ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ↔ ( 𝑦 ∈ ω ∧ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ) )
38	37	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ω ∧ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ) }
39		omex	⊢ ω ∈ V
40		id	⊢ ( ω ∈ V → ω ∈ V )
41		unab	⊢ ( { 𝑥 ∣ ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) } ∪ { 𝑥 ∣ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) } ) = { 𝑥 ∣ ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) }
42	31	abrexex	⊢ { 𝑥 ∣ ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) } ∈ V
43	39	abrexex	⊢ { 𝑥 ∣ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) } ∈ V
44	42 43	unex	⊢ ( { 𝑥 ∣ ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) } ∪ { 𝑥 ∣ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) } ) ∈ V
45	41 44	eqeltrri	⊢ { 𝑥 ∣ ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) } ∈ V
46	45	a1i	⊢ ( ( ( ω ∈ V ∧ 𝑦 ∈ ω ) ∧ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → { 𝑥 ∣ ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) } ∈ V )
47	46	ralrimiva	⊢ ( ( ω ∈ V ∧ 𝑦 ∈ ω ) → ∀ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) { 𝑥 ∣ ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) } ∈ V )
48		abrexex2g	⊢ ( ( ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∈ V ∧ ∀ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) { 𝑥 ∣ ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) } ∈ V ) → { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) } ∈ V )
49	31 47 48	sylancr	⊢ ( ( ω ∈ V ∧ 𝑦 ∈ ω ) → { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) } ∈ V )
50	40 49	opabex3rd	⊢ ( ω ∈ V → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ω ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ∈ V )
51	39 50	ax-mp	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ω ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ∈ V
52		simpr	⊢ ( ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) → ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) )
53	52	anim2i	⊢ ( ( 𝑦 ∈ ω ∧ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ) → ( 𝑦 ∈ ω ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
54	53	ssopab2i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ω ∧ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ω ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) }
55	51 54	ssexi	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ω ∧ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ) } ∈ V
56	55	a1i	⊢ ( 𝑁 ∈ ω → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ω ∧ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ) } ∈ V )
57	38 56	eqeltrid	⊢ ( 𝑁 ∈ ω → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ∈ V )
58		unexg	⊢ ( ( ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∈ V ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ∈ V ) → ( ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ∈ V )
59	31 57 58	sylancr	⊢ ( 𝑁 ∈ ω → ( ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ∈ V )
60	22 30 32 59	fvmptd	⊢ ( 𝑁 ∈ ω → ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) = ( ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
61	21 60	eqtrd	⊢ ( 𝑁 ∈ ω → ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) ) = ( ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
62	61	dmeqd	⊢ ( 𝑁 ∈ ω → dom ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) ) = dom ( ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
63		dmun	⊢ dom ( ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) = ( dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∪ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } )
64	62 63	eqtrdi	⊢ ( 𝑁 ∈ ω → dom ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) ) = ( dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∪ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
65		fmlafv	⊢ ( 𝑁 ∈ suc ω → ( Fmla ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
66	17 65	syl	⊢ ( 𝑁 ∈ ω → ( Fmla ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
67	66	eqcomd	⊢ ( 𝑁 ∈ ω → dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) = ( Fmla ‘ 𝑁 ) )
68		dmopab	⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) }
69	68	a1i	⊢ ( 𝑁 ∈ ω → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } )
70		0ex	⊢ ∅ ∈ V
71	70	isseti	⊢ ∃ 𝑦 𝑦 = ∅
72		19.41v	⊢ ( ∃ 𝑦 ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ↔ ( ∃ 𝑦 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
73	71 72	mpbiran	⊢ ( ∃ 𝑦 ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ↔ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) )
74	73	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } = { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) }
75	69 74	eqtrdi	⊢ ( 𝑁 ∈ ω → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } = { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) } )
76	67 75	uneq12d	⊢ ( 𝑁 ∈ ω → ( dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∪ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) } ) )
77	64 76	eqtrd	⊢ ( 𝑁 ∈ ω → dom ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) } ) )
78	9 16 77	3eqtrd	⊢ ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) } ) )

Metamath Proof Explorer

Theorem fmlasuc0

Proof