Metamath Proof Explorer


Theorem fmla0

Description: The valid Godel formulas of height 0 is the set of all formulas of the form v_i e. v_j ("Godel-set of membership") coded as <. (/) , <. i , j >. >. . (Contributed by AV, 14-Sep-2023)

Ref Expression
Assertion fmla0 ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) }

Proof

Step Hyp Ref Expression
1 peano1 ∅ ∈ ω
2 elelsuc ( ∅ ∈ ω → ∅ ∈ suc ω )
3 fmlafv ( ∅ ∈ suc ω → ( Fmla ‘ ∅ ) = dom ( ( ∅ Sat ∅ ) ‘ ∅ ) )
4 1 2 3 mp2b ( Fmla ‘ ∅ ) = dom ( ( ∅ Sat ∅ ) ‘ ∅ )
5 satf00 ( ( ∅ Sat ∅ ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) }
6 5 dmeqi dom ( ( ∅ Sat ∅ ) ‘ ∅ ) = dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) }
7 0ex ∅ ∈ V
8 7 isseti 𝑦 𝑦 = ∅
9 19.41v ( ∃ 𝑦 ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ↔ ( ∃ 𝑦 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) )
10 8 9 mpbiran ( ∃ 𝑦 ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) )
11 10 abbii { 𝑥 ∣ ∃ 𝑦 ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) } = { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) }
12 dmopab dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) }
13 rabab { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) } = { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) }
14 11 12 13 3eqtr4i dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) } = { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) }
15 4 6 14 3eqtri ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) }