Metamath Proof Explorer


Theorem satf0n0

Description: The value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation does not contain the empty set. (Contributed by AV, 19-Sep-2023)

Ref Expression
Assertion satf0n0 N ω Sat N

Proof

Step Hyp Ref Expression
1 fveq2 x = Sat x = Sat
2 1 eleq2d x = Sat x Sat
3 2 notbid x = ¬ Sat x ¬ Sat
4 fveq2 x = y Sat x = Sat y
5 4 eleq2d x = y Sat x Sat y
6 5 notbid x = y ¬ Sat x ¬ Sat y
7 fveq2 x = suc y Sat x = Sat suc y
8 7 eleq2d x = suc y Sat x Sat suc y
9 8 notbid x = suc y ¬ Sat x ¬ Sat suc y
10 fveq2 x = N Sat x = Sat N
11 10 eleq2d x = N Sat x Sat N
12 11 notbid x = N ¬ Sat x ¬ Sat N
13 0nelopab ¬ x y | y = i ω j ω x = i 𝑔 j
14 satf00 Sat = x y | y = i ω j ω x = i 𝑔 j
15 14 eleq2i Sat x y | y = i ω j ω x = i 𝑔 j
16 13 15 mtbir ¬ Sat
17 simpr y ω ¬ Sat y ¬ Sat y
18 0nelopab ¬ x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
19 ioran ¬ Sat y x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u ¬ Sat y ¬ x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
20 17 18 19 sylanblrc y ω ¬ Sat 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
21 eqid Sat = Sat
22 21 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
23 22 adantr y ω ¬ Sat 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
24 23 eleq2d y ω ¬ Sat 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
25 elun Sat y x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u Sat y x z | z = u Sat y v Sat y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
26 24 25 bitrdi y ω ¬ Sat 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
27 20 26 mtbird y ω ¬ Sat y ¬ Sat suc y
28 27 ex y ω ¬ Sat y ¬ Sat suc y
29 3 6 9 12 16 28 finds N ω ¬ Sat N
30 df-nel Sat N ¬ Sat N
31 29 30 sylibr N ω Sat N