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 \in ω \land J \in ω \land X \in V) \to \neg \{X\} ⊧ (I \in_{𝑔} J)$

Proof

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

Metamath Proof Explorer

Theorem prv1n

Proof