satf0suc

Description: The value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation at a successor. (Contributed by AV, 19-Sep-2023)

		Ref	Expression
	Hypothesis	satf0suc.s	⊢ 𝑆 = ( ∅ Sat ∅ )
	Assertion	satf0suc	⊢ ( 𝑁 ∈ ω → ( 𝑆 ‘ suc 𝑁 ) = ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		satf0suc.s	⊢ 𝑆 = ( ∅ Sat ∅ )
2	1	fveq1i	⊢ ( 𝑆 ‘ suc 𝑁 ) = ( ( ∅ Sat ∅ ) ‘ suc 𝑁 )
3	2	a1i	⊢ ( 𝑁 ∈ ω → ( 𝑆 ‘ suc 𝑁 ) = ( ( ∅ Sat ∅ ) ‘ suc 𝑁 ) )
4		omsucelsucb	⊢ ( 𝑁 ∈ ω ↔ suc 𝑁 ∈ suc ω )
5		satf0sucom	⊢ ( suc 𝑁 ∈ suc ω → ( ( ∅ Sat ∅ ) ‘ suc 𝑁 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ suc 𝑁 ) )
6	4 5	sylbi	⊢ ( 𝑁 ∈ ω → ( ( ∅ Sat ∅ ) ‘ suc 𝑁 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ suc 𝑁 ) )
7		nnon	⊢ ( 𝑁 ∈ ω → 𝑁 ∈ On )
8		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 ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) ) )
9	7 8	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 ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) ) )
10		elelsuc	⊢ ( 𝑁 ∈ ω → 𝑁 ∈ suc ω )
11		satf0sucom	⊢ ( 𝑁 ∈ suc ω → ( ( ∅ Sat ∅ ) ‘ 𝑁 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) )
12	10 11	syl	⊢ ( 𝑁 ∈ ω → ( ( ∅ Sat ∅ ) ‘ 𝑁 ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) )
13	1	eqcomi	⊢ ( ∅ Sat ∅ ) = 𝑆
14	13	fveq1i	⊢ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) = ( 𝑆 ‘ 𝑁 )
15	12 14	eqtr3di	⊢ ( 𝑁 ∈ ω → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) = ( 𝑆 ‘ 𝑁 ) )
16	15	fveq2d	⊢ ( 𝑁 ∈ ω → ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ 𝑁 ) ) = ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( 𝑆 ‘ 𝑁 ) ) )
17		eqidd	⊢ ( 𝑁 ∈ ω → ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) = ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) )
18		id	⊢ ( 𝑓 = ( 𝑆 ‘ 𝑁 ) → 𝑓 = ( 𝑆 ‘ 𝑁 ) )
19		rexeq	⊢ ( 𝑓 = ( 𝑆 ‘ 𝑁 ) → ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ↔ ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
20	19	orbi1d	⊢ ( 𝑓 = ( 𝑆 ‘ 𝑁 ) → ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ↔ ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
21	20	rexeqbi1dv	⊢ ( 𝑓 = ( 𝑆 ‘ 𝑁 ) → ( ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ↔ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
22	21	anbi2d	⊢ ( 𝑓 = ( 𝑆 ‘ 𝑁 ) → ( ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ↔ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ) )
23	22	opabbidv	⊢ ( 𝑓 = ( 𝑆 ‘ 𝑁 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } )
24	18 23	uneq12d	⊢ ( 𝑓 = ( 𝑆 ‘ 𝑁 ) → ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) = ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
25	24	adantl	⊢ ( ( 𝑁 ∈ ω ∧ 𝑓 = ( 𝑆 ‘ 𝑁 ) ) → ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) = ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
26		fvex	⊢ ( 𝑆 ‘ 𝑁 ) ∈ V
27	26	a1i	⊢ ( 𝑁 ∈ ω → ( 𝑆 ‘ 𝑁 ) ∈ V )
28		omex	⊢ ω ∈ V
29		satf0suclem	⊢ ( ( ( 𝑆 ‘ 𝑁 ) ∈ V ∧ ( 𝑆 ‘ 𝑁 ) ∈ V ∧ ω ∈ V ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ∈ V )
30	26 26 28 29	mp3an	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ∈ V
31	26 30	unex	⊢ ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ∈ V
32	31	a1i	⊢ ( 𝑁 ∈ ω → ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ∈ V )
33	17 25 27 32	fvmptd	⊢ ( 𝑁 ∈ ω → ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ‘ ( 𝑆 ‘ 𝑁 ) ) = ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
34	9 16 33	3eqtrd	⊢ ( 𝑁 ∈ ω → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ‘ suc 𝑁 ) = ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
35	3 6 34	3eqtrd	⊢ ( 𝑁 ∈ ω → ( 𝑆 ‘ suc 𝑁 ) = ( ( 𝑆 ‘ 𝑁 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )

Metamath Proof Explorer

Theorem satf0suc

Proof