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 e. _om /\ J e. _om /\ X e. V ) -> -. { X } |= ( I e.g J ) )

Proof

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