Metamath Proof Explorer


Theorem prv1n

Description: No wff encoded as a Godel-set of membership is true in a model with only one element. (Contributed by AV, 19-Nov-2023)

Ref Expression
Assertion prv1n I ω J ω X V ¬ X I 𝑔 J

Proof

Step Hyp Ref Expression
1 eqid ω × X = ω × X
2 omex ω V
3 snex X V
4 2 3 xpex ω × X V
5 eqeq1 a = ω × X a = ω × X ω × X = ω × X
6 4 5 spcev ω × X = ω × X a a = ω × X
7 1 6 mp1i I ω J ω X V a a = ω × X
8 3 2 pm3.2i X V ω V
9 elmapg X V ω V a X ω a : ω X
10 8 9 mp1i I ω J ω X V a X ω a : ω X
11 fconst2g X V a : ω X a = ω × X
12 11 3ad2ant3 I ω J ω X V a : ω X a = ω × X
13 10 12 bitrd I ω J ω X V a X ω a = ω × X
14 13 exbidv I ω J ω X V a a X ω a a = ω × X
15 7 14 mpbird I ω J ω X V a a X ω
16 neq0 ¬ X ω = a a X ω
17 15 16 sylibr I ω J ω X V ¬ X ω =
18 eqcom X ω = = X ω
19 17 18 sylnib I ω J ω X V ¬ = X ω
20 ovex I 𝑔 J V
21 3 20 pm3.2i X V I 𝑔 J V
22 prv X V I 𝑔 J V X I 𝑔 J X Sat I 𝑔 J = X ω
23 21 22 mp1i I ω J ω X V X I 𝑔 J X Sat I 𝑔 J = X ω
24 goel I ω J ω I 𝑔 J = I J
25 0ex V
26 25 snid
27 26 a1i I ω J ω
28 opelxpi I ω J ω I J ω × ω
29 27 28 opelxpd I ω J ω I J × ω × ω
30 24 29 eqeltrd I ω J ω I 𝑔 J × ω × ω
31 fmla0xp Fmla = × ω × ω
32 30 31 eleqtrrdi I ω J ω I 𝑔 J Fmla
33 32 3adant3 I ω J ω X V I 𝑔 J Fmla
34 satefvfmla0 X V I 𝑔 J Fmla X Sat I 𝑔 J = a X ω | a 1 st 2 nd I 𝑔 J a 2 nd 2 nd I 𝑔 J
35 3 33 34 sylancr I ω J ω X V X Sat I 𝑔 J = a X ω | a 1 st 2 nd I 𝑔 J a 2 nd 2 nd I 𝑔 J
36 24 fveq2d I ω J ω 2 nd I 𝑔 J = 2 nd I J
37 opex I J V
38 25 37 op2nd 2 nd I J = I J
39 36 38 eqtrdi I ω J ω 2 nd I 𝑔 J = I J
40 39 fveq2d I ω J ω 1 st 2 nd I 𝑔 J = 1 st I J
41 op1stg I ω J ω 1 st I J = I
42 40 41 eqtrd I ω J ω 1 st 2 nd I 𝑔 J = I
43 42 fveq2d I ω J ω a 1 st 2 nd I 𝑔 J = a I
44 39 fveq2d I ω J ω 2 nd 2 nd I 𝑔 J = 2 nd I J
45 op2ndg I ω J ω 2 nd I J = J
46 44 45 eqtrd I ω J ω 2 nd 2 nd I 𝑔 J = J
47 46 fveq2d I ω J ω a 2 nd 2 nd I 𝑔 J = a J
48 43 47 eleq12d I ω J ω a 1 st 2 nd I 𝑔 J a 2 nd 2 nd I 𝑔 J a I a J
49 48 rabbidv I ω J ω a X ω | a 1 st 2 nd I 𝑔 J a 2 nd 2 nd I 𝑔 J = a X ω | a I a J
50 49 3adant3 I ω J ω X V a X ω | a 1 st 2 nd I 𝑔 J a 2 nd 2 nd I 𝑔 J = a X ω | a I a J
51 elmapi a X ω a : ω X
52 elirr ¬ X X
53 fvconst a : ω X I ω a I = X
54 53 3ad2antr1 a : ω X I ω J ω X V a I = X
55 fvconst a : ω X J ω a J = X
56 55 3ad2antr2 a : ω X I ω J ω X V a J = X
57 54 56 eleq12d a : ω X I ω J ω X V a I a J X X
58 52 57 mtbiri a : ω X I ω J ω X V ¬ a I a J
59 58 ex a : ω X I ω J ω X V ¬ a I a J
60 51 59 syl a X ω I ω J ω X V ¬ a I a J
61 60 impcom I ω J ω X V a X ω ¬ a I a J
62 61 ralrimiva I ω J ω X V a X ω ¬ a I a J
63 rabeq0 a X ω | a I a J = a X ω ¬ a I a J
64 62 63 sylibr I ω J ω X V a X ω | a I a J =
65 50 64 eqtrd I ω J ω X V a X ω | a 1 st 2 nd I 𝑔 J a 2 nd 2 nd I 𝑔 J =
66 35 65 eqtrd I ω J ω X V X Sat I 𝑔 J =
67 66 eqeq1d I ω J ω X V X Sat I 𝑔 J = X ω = X ω
68 23 67 bitrd I ω J ω X V X I 𝑔 J = X ω
69 19 68 mtbird I ω J ω X V ¬ X I 𝑔 J