Theorem satf00

Description: The value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation at (/) . (Contributed by AV, 14-Sep-2023)

	Ref	Expression
Assertion	satf00	⊢ ( ( ∅ Sat ∅ ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) }

Proof

Step	Hyp	Ref	Expression
1		peano1	⊢ ∅ ∈ ω
2		elelsuc	⊢ ( ∅ ∈ ω → ∅ ∈ suc ω )
3		satf0sucom	⊢ ( ∅ ∈ suc ω → ( ( ∅ Sat ∅ ) ‘ ∅ ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ) ‘ ∅ ) )
4	1 2 3	mp2b	⊢ ( ( ∅ Sat ∅ ) ‘ ∅ ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ) ‘ ∅ )
5		omex	⊢ ω ∈ V
6	5 5	xpex	⊢ ( ω × ω ) ∈ V
7		xpexg	⊢ ( ( ω ∈ V ∧ ( ω × ω ) ∈ V ) → ( ω × ( ω × ω ) ) ∈ V )
8		simpl	⊢ ( ( ω ∈ V ∧ ( ω × ω ) ∈ V ) → ω ∈ V )
9		goelel3xp	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑖 ∈𝑔 𝑗 ) ∈ ( ω × ( ω × ω ) ) )
10		eleq1	⊢ ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) → ( 𝑥 ∈ ( ω × ( ω × ω ) ) ↔ ( 𝑖 ∈𝑔 𝑗 ) ∈ ( ω × ( ω × ω ) ) ) )
11	9 10	syl5ibrcom	⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) → 𝑥 ∈ ( ω × ( ω × ω ) ) ) )
12	11	rexlimivv	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) → 𝑥 ∈ ( ω × ( ω × ω ) ) )
13	12	ad2antll	⊢ ( ( ( ω ∈ V ∧ ( ω × ω ) ∈ V ) ∧ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) ) → 𝑥 ∈ ( ω × ( ω × ω ) ) )
14		eleq1	⊢ ( 𝑦 = ∅ → ( 𝑦 ∈ ω ↔ ∅ ∈ ω ) )
15	1 14	mpbiri	⊢ ( 𝑦 = ∅ → 𝑦 ∈ ω )
16	15	ad2antrl	⊢ ( ( ( ω ∈ V ∧ ( ω × ω ) ∈ V ) ∧ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) ) → 𝑦 ∈ ω )
17	7 8 13 16	opabex2	⊢ ( ( ω ∈ V ∧ ( ω × ω ) ∈ V ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ∈ V )
18	5 6 17	mp2an	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ∈ V
19	18	rdg0	⊢ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) } ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) }
20	4 19	eqtri	⊢ ( ( ∅ Sat ∅ ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) }