Metamath Proof Explorer


Theorem fmlafvel

Description: A class is a valid Godel formula of height N iff it is the first component of a member of the value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation at N . (Contributed by AV, 19-Sep-2023)

Ref Expression
Assertion fmlafvel N ω F Fmla N F Sat N

Proof

Step Hyp Ref Expression
1 fveq2 x = Fmla x = Fmla
2 1 eleq2d x = F Fmla x F Fmla
3 fveq2 x = Sat x = Sat
4 3 eleq2d x = F Sat x F Sat
5 2 4 bibi12d x = F Fmla x F Sat x F Fmla F Sat
6 5 imbi2d x = F V F Fmla x F Sat x F V F Fmla F Sat
7 fveq2 x = y Fmla x = Fmla y
8 7 eleq2d x = y F Fmla x F Fmla y
9 fveq2 x = y Sat x = Sat y
10 9 eleq2d x = y F Sat x F Sat y
11 8 10 bibi12d x = y F Fmla x F Sat x F Fmla y F Sat y
12 11 imbi2d x = y F V F Fmla x F Sat x F V F Fmla y F Sat y
13 fveq2 x = suc y Fmla x = Fmla suc y
14 13 eleq2d x = suc y F Fmla x F Fmla suc y
15 fveq2 x = suc y Sat x = Sat suc y
16 15 eleq2d x = suc y F Sat x F Sat suc y
17 14 16 bibi12d x = suc y F Fmla x F Sat x F Fmla suc y F Sat suc y
18 17 imbi2d x = suc y F V F Fmla x F Sat x F V F Fmla suc y F Sat suc y
19 fveq2 x = N Fmla x = Fmla N
20 19 eleq2d x = N F Fmla x F Fmla N
21 fveq2 x = N Sat x = Sat N
22 21 eleq2d x = N F Sat x F Sat N
23 20 22 bibi12d x = N F Fmla x F Sat x F Fmla N F Sat N
24 23 imbi2d x = N F V F Fmla x F Sat x F V F Fmla N F Sat N
25 eqeq1 x = F x = i 𝑔 j F = i 𝑔 j
26 25 2rexbidv x = F i ω j ω x = i 𝑔 j i ω j ω F = i 𝑔 j
27 26 elrab F x V | i ω j ω x = i 𝑔 j F V i ω j ω F = i 𝑔 j
28 eqidd F V i ω j ω F = i 𝑔 j =
29 simpr F V i ω j ω F = i 𝑔 j i ω j ω F = i 𝑔 j
30 28 29 jca F V i ω j ω F = i 𝑔 j = i ω j ω F = i 𝑔 j
31 simpr = i ω j ω F = i 𝑔 j i ω j ω F = i 𝑔 j
32 31 anim2i F V = i ω j ω F = i 𝑔 j F V i ω j ω F = i 𝑔 j
33 32 ex F V = i ω j ω F = i 𝑔 j F V i ω j ω F = i 𝑔 j
34 30 33 impbid2 F V F V i ω j ω F = i 𝑔 j = i ω j ω F = i 𝑔 j
35 27 34 syl5bb F V F x V | i ω j ω x = i 𝑔 j = i ω j ω F = i 𝑔 j
36 fmla0 Fmla = x V | i ω j ω x = i 𝑔 j
37 36 eleq2i F Fmla F x V | i ω j ω x = i 𝑔 j
38 37 a1i F V F Fmla F x V | i ω j ω x = i 𝑔 j
39 satf00 Sat = x y | y = i ω j ω x = i 𝑔 j
40 39 a1i F V Sat = x y | y = i ω j ω x = i 𝑔 j
41 40 eleq2d F V F Sat F x y | y = i ω j ω x = i 𝑔 j
42 0ex V
43 eqeq1 y = y = =
44 43 26 bi2anan9r x = F y = y = i ω j ω x = i 𝑔 j = i ω j ω F = i 𝑔 j
45 44 opelopabga F V V F x y | y = i ω j ω x = i 𝑔 j = i ω j ω F = i 𝑔 j
46 42 45 mpan2 F V F x y | y = i ω j ω x = i 𝑔 j = i ω j ω F = i 𝑔 j
47 41 46 bitrd F V F Sat = i ω j ω F = i 𝑔 j
48 35 38 47 3bitr4d F V F Fmla F Sat
49 eqid =
50 49 biantrur u Sat y v Sat y F = 1 st u 𝑔 1 st v i ω F = 𝑔 i 1 st u = u Sat y v Sat y F = 1 st u 𝑔 1 st v i ω F = 𝑔 i 1 st u
51 50 bicomi = u Sat y v Sat y F = 1 st u 𝑔 1 st v i ω F = 𝑔 i 1 st u u Sat y v Sat y F = 1 st u 𝑔 1 st v i ω F = 𝑔 i 1 st u
52 51 a1i F V = u Sat y v Sat y F = 1 st u 𝑔 1 st v i ω F = 𝑔 i 1 st u u Sat y v Sat y F = 1 st u 𝑔 1 st v i ω F = 𝑔 i 1 st u
53 eqeq1 z = z = =
54 eqeq1 x = F x = 1 st u 𝑔 1 st v F = 1 st u 𝑔 1 st v
55 54 rexbidv x = F v Sat y x = 1 st u 𝑔 1 st v v Sat y F = 1 st u 𝑔 1 st v
56 eqeq1 x = F x = 𝑔 i 1 st u F = 𝑔 i 1 st u
57 56 rexbidv x = F i ω x = 𝑔 i 1 st u i ω F = 𝑔 i 1 st u
58 55 57 orbi12d x = F v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u v Sat y F = 1 st u 𝑔 1 st v i ω F = 𝑔 i 1 st u
59 58 rexbidv x = F u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u u Sat y v Sat y F = 1 st u 𝑔 1 st v i ω F = 𝑔 i 1 st u
60 53 59 bi2anan9r x = F z = z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = u Sat y v Sat y F = 1 st u 𝑔 1 st v i ω F = 𝑔 i 1 st u
61 60 opelopabga F V V F x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = u Sat y v Sat y F = 1 st u 𝑔 1 st v i ω F = 𝑔 i 1 st u
62 42 61 mpan2 F V F x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = u Sat y v Sat y F = 1 st u 𝑔 1 st v i ω F = 𝑔 i 1 st u
63 59 elabg F V F x | u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u u Sat y v Sat y F = 1 st u 𝑔 1 st v i ω F = 𝑔 i 1 st u
64 52 62 63 3bitr4d F V F x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u F x | u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
65 64 adantl y ω F V F Fmla y F Sat y F V F x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u F x | u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
66 65 orbi2d y ω F V F Fmla y F Sat y F V F Sat y F x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u F Sat y F x | u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
67 eqid Sat = Sat
68 67 satf0suc y ω Sat suc y = Sat y x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
69 68 eleq2d y ω F Sat suc y F Sat y x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
70 elun F Sat y x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u F Sat y F x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
71 69 70 bitrdi y ω F Sat suc y F Sat y F x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
72 71 ad2antrr y ω F V F Fmla y F Sat y F V F Sat suc y F Sat y F x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
73 fmlasuc0 y ω Fmla suc y = Fmla y x | u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
74 73 eleq2d y ω F Fmla suc y F Fmla y x | u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
75 74 ad2antrr y ω F V F Fmla y F Sat y F V F Fmla suc y F Fmla y x | u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
76 elun F Fmla y x | u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u F Fmla y F x | u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
77 76 a1i y ω F V F Fmla y F Sat y F V F Fmla y x | u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u F Fmla y F x | u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
78 simpr y ω F V F Fmla y F Sat y F V F Fmla y F Sat y
79 78 imp y ω F V F Fmla y F Sat y F V F Fmla y F Sat y
80 79 orbi1d y ω F V F Fmla y F Sat y F V F Fmla y F x | u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u F Sat y F x | u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
81 75 77 80 3bitrd y ω F V F Fmla y F Sat y F V F Fmla suc y F Sat y F x | u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
82 66 72 81 3bitr4rd y ω F V F Fmla y F Sat y F V F Fmla suc y F Sat suc y
83 82 exp31 y ω F V F Fmla y F Sat y F V F Fmla suc y F Sat suc y
84 6 12 18 24 48 83 finds N ω F V F Fmla N F Sat N
85 84 com12 F V N ω F Fmla N F Sat N
86 prcnel ¬ F V ¬ F Fmla N
87 86 adantr ¬ F V N ω ¬ F Fmla N
88 opprc1 ¬ F V F =
89 88 adantr ¬ F V N ω F =
90 satf0n0 N ω Sat N
91 df-nel Sat N ¬ Sat N
92 90 91 sylib N ω ¬ Sat N
93 92 adantl ¬ F V N ω ¬ Sat N
94 89 93 eqneltrd ¬ F V N ω ¬ F Sat N
95 87 94 2falsed ¬ F V N ω F Fmla N F Sat N
96 95 ex ¬ F V N ω F Fmla N F Sat N
97 85 96 pm2.61i N ω F Fmla N F Sat N