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 ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝑋𝑉 ) → ¬ { 𝑋 } ⊧ ( 𝐼𝑔 𝐽 ) )

Proof

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