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

Metamath Proof Explorer

Theorem fmla0xp

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, 15-Sep-2023)

Ref Expression
Assertion fmla0xp ( Fmla ‘ ∅ ) = ( { ∅ } × ( ω × ω ) )

Proof

Step Hyp Ref Expression
1 fmla0 ⊢ ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) }
2 rabab ⊢ { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } = { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) }
3 eqabcb ⊢ ( { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } = ( { ∅ } × ( ω × ω ) ) ↔ ∀ 𝑥 ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) ) )
4 goel ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑖 ∈𝑔 𝑗 ) = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
5 4 eqeq2d ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
6 5 2rexbiia ⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
7 0ex ⊢ ∅ ∈ V
8 7 snid ⊢ ∅ ∈ { ∅ }
9 8 a1i ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ∅ ∈ { ∅ } )
10 opelxpi ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ⟨ 𝑖 , 𝑗 ⟩ ∈ ( ω × ω ) )
11 9 10 opelxpd ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ∈ ( { ∅ } × ( ω × ω ) ) )
12 eleq1 ⊢ ( 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → ( 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) ↔ ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ∈ ( { ∅ } × ( ω × ω ) ) ) )
13 11 12 syl5ibrcom ⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) ) )
14 13 rexlimivv ⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ → 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) )
15 elxpi ⊢ ( 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) → ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ { ∅ } ∧ 𝑧 ∈ ( ω × ω ) ) ) )
16 elsni ⊢ ( 𝑦 ∈ { ∅ } → 𝑦 = ∅ )
17 16 opeq1d ⊢ ( 𝑦 ∈ { ∅ } → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ ∅ , 𝑧 ⟩ )
18 17 eqeq2d ⊢ ( 𝑦 ∈ { ∅ } → ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ↔ 𝑥 = ⟨ ∅ , 𝑧 ⟩ ) )
19 18 adantr ⊢ ( ( 𝑦 ∈ { ∅ } ∧ 𝑧 ∈ ( ω × ω ) ) → ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ↔ 𝑥 = ⟨ ∅ , 𝑧 ⟩ ) )
20 elxpi ⊢ ( 𝑧 ∈ ( ω × ω ) → ∃ 𝑖 ∃ 𝑗 ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) )
21 simprr ⊢ ( ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ ∧ ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ) → ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) )
22 simpl ⊢ ( ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ ∧ ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ) → 𝑥 = ⟨ ∅ , 𝑧 ⟩ )
23 opeq2 ⊢ ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ → ⟨ ∅ , 𝑧 ⟩ = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
24 23 adantr ⊢ ( ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ⟨ ∅ , 𝑧 ⟩ = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
25 24 adantl ⊢ ( ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ ∧ ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ) → ⟨ ∅ , 𝑧 ⟩ = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
26 22 25 eqtrd ⊢ ( ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ ∧ ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ) → 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
27 21 26 jca ⊢ ( ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ ∧ ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) ) → ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
28 27 ex ⊢ ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ → ( ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) ) )
29 28 2eximdv ⊢ ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ → ( ∃ 𝑖 ∃ 𝑗 ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ∃ 𝑖 ∃ 𝑗 ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) ) )
30 r2ex ⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ↔ ∃ 𝑖 ∃ 𝑗 ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ∧ 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
31 29 30 imbitrrdi ⊢ ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ → ( ∃ 𝑖 ∃ 𝑗 ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
32 20 31 syl5com ⊢ ( 𝑧 ∈ ( ω × ω ) → ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
33 32 adantl ⊢ ( ( 𝑦 ∈ { ∅ } ∧ 𝑧 ∈ ( ω × ω ) ) → ( 𝑥 = ⟨ ∅ , 𝑧 ⟩ → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
34 19 33 sylbid ⊢ ( ( 𝑦 ∈ { ∅ } ∧ 𝑧 ∈ ( ω × ω ) ) → ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ) )
35 34 impcom ⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ { ∅ } ∧ 𝑧 ∈ ( ω × ω ) ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
36 35 exlimivv ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ { ∅ } ∧ 𝑧 ∈ ( ω × ω ) ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
37 15 36 syl ⊢ ( 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ )
38 14 37 impbii ⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ⟨ ∅ , ⟨ 𝑖 , 𝑗 ⟩ ⟩ ↔ 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) )
39 6 38 bitri ⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝑥 ∈ ( { ∅ } × ( ω × ω ) ) )
40 3 39 mpgbir ⊢ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } = ( { ∅ } × ( ω × ω ) )
41 1 2 40 3eqtri ⊢ ( Fmla ‘ ∅ ) = ( { ∅ } × ( ω × ω ) )