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