This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∅ ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ) }