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 ⁡ ∅ = x ∈ V | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j

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 ∅ ⁡ ∅ = x y | y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j
6 5 dmeqi ⊢ dom ⁡ ∅ Sat ∅ ⁡ ∅ = dom ⁡ x y | y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j
7 0ex ⊢ ∅ ∈ V
8 7 isseti ⊢ ∃ y y = ∅
9 19.41v ⊢ ∃ y y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ↔ ∃ y y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j
10 8 9 mpbiran ⊢ ∃ y y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j ↔ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j
11 10 abbii ⊢ x | ∃ y y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j = x | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j
12 dmopab ⊢ dom ⁡ x y | y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j = x | ∃ y y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j
13 rabab ⊢ x ∈ V | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j = x | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j
14 11 12 13 3eqtr4i ⊢ dom ⁡ x y | y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j = x ∈ V | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j
15 4 6 14 3eqtri ⊢ Fmla ⁡ ∅ = x ∈ V | ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j