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 = x V | i ω j ω x = i 𝑔 j
2 rabab x V | i ω j ω x = i 𝑔 j = x | i ω j ω x = i 𝑔 j
3 abeq1 x | i ω j ω x = i 𝑔 j = × ω × ω x i ω j ω x = i 𝑔 j x × ω × ω
4 goel i ω j ω i 𝑔 j = i j
5 4 eqeq2d i ω j ω x = i 𝑔 j x = i j
6 5 2rexbiia i ω j ω x = i 𝑔 j i ω j ω x = i j
7 0ex V
8 7 snid
9 8 a1i i ω j ω
10 opelxpi i ω j ω i j ω × ω
11 9 10 opelxpd i ω j ω i j × ω × ω
12 eleq1 x = i j x × ω × ω i j × ω × ω
13 11 12 syl5ibrcom i ω j ω x = i j x × ω × ω
14 13 rexlimivv i ω j ω x = i j x × ω × ω
15 elxpi x × ω × ω y z x = y z y z ω × ω
16 elsni y y =
17 16 opeq1d y y z = z
18 17 eqeq2d y x = y z x = z
19 18 adantr y z ω × ω x = y z x = z
20 elxpi z ω × ω i j z = i j i ω j ω
21 simprr x = z z = i j i ω j ω i ω j ω
22 simpl x = z z = i j i ω j ω x = z
23 opeq2 z = i j z = i j
24 23 adantr z = i j i ω j ω z = i j
25 24 adantl x = z z = i j i ω j ω z = i j
26 22 25 eqtrd x = z z = i j i ω j ω x = i j
27 21 26 jca x = z z = i j i ω j ω i ω j ω x = i j
28 27 ex x = z z = i j i ω j ω i ω j ω x = i j
29 28 2eximdv x = z i j z = i j i ω j ω i j i ω j ω x = i j
30 r2ex i ω j ω x = i j i j i ω j ω x = i j
31 29 30 syl6ibr x = z i j z = i j i ω j ω i ω j ω x = i j
32 20 31 syl5com z ω × ω x = z i ω j ω x = i j
33 32 adantl y z ω × ω x = z i ω j ω x = i j
34 19 33 sylbid y z ω × ω x = y z i ω j ω x = i j
35 34 impcom x = y z y z ω × ω i ω j ω x = i j
36 35 exlimivv y z x = y z y z ω × ω i ω j ω x = i j
37 15 36 syl x × ω × ω i ω j ω x = i j
38 14 37 impbii i ω j ω x = i j x × ω × ω
39 6 38 bitri i ω j ω x = i 𝑔 j x × ω × ω
40 3 39 mpgbir x | i ω j ω x = i 𝑔 j = × ω × ω
41 1 2 40 3eqtri Fmla = × ω × ω