Metamath Proof Explorer

Theorem elnanelprv

Description: The wff ( A e. B -/\ B e. A ) encoded as ( ( A e.g B ) |g ( B e.g A ) ) is true in any model M . This is the model theoretic proof of elnanel . (Contributed by AV, 5-Nov-2023)

		Ref	Expression
	Assertion	elnanelprv	$⊢ (M \in V \land A \in ω \land B \in ω) \to M ⊧ ((A \in_{𝑔} B) ⊼_{𝑔} (B \in_{𝑔} A))$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (M \in V \land A \in ω \land B \in ω) \to M \in V$
2		3simpc	$⊢ (M \in V \land A \in ω \land B \in ω) \to (A \in ω \land B \in ω)$
3		pm3.22	$⊢ (A \in ω \land B \in ω) \to (B \in ω \land A \in ω)$
4	3	3adant1	$⊢ (M \in V \land A \in ω \land B \in ω) \to (B \in ω \land A \in ω)$
5		eqid	$⊢ (A \in_{𝑔} B) ⊼_{𝑔} (B \in_{𝑔} A) = (A \in_{𝑔} B) ⊼_{𝑔} (B \in_{𝑔} A)$
6	5	satefvfmla1	$⊢ (M \in V \land (A \in ω \land B \in ω) \land (B \in ω \land A \in ω)) \to M {Sat}_{\in} ((A \in_{𝑔} B) ⊼_{𝑔} (B \in_{𝑔} A)) = \{a \in (M^{ω}) \| (\neg a (A) \in a (B) \lor \neg a (B) \in a (A))\}$
7	1 2 4 6	syl3anc	$⊢ (M \in V \land A \in ω \land B \in ω) \to M {Sat}_{\in} ((A \in_{𝑔} B) ⊼_{𝑔} (B \in_{𝑔} A)) = \{a \in (M^{ω}) \| (\neg a (A) \in a (B) \lor \neg a (B) \in a (A))\}$
8		elnanel	$⊢ (a (A) \in a (B) ⊼ a (B) \in a (A))$
9		nanor	$⊢ (a (A) \in a (B) ⊼ a (B) \in a (A)) \leftrightarrow (\neg a (A) \in a (B) \lor \neg a (B) \in a (A))$
10	8 9	mpbi	$⊢ (\neg a (A) \in a (B) \lor \neg a (B) \in a (A))$
11	10	a1i	$⊢ a \in (M^{ω}) \to (\neg a (A) \in a (B) \lor \neg a (B) \in a (A))$
12	11	rabeqc	$⊢ \{a \in (M^{ω}) \| (\neg a (A) \in a (B) \lor \neg a (B) \in a (A))\} = M^{ω}$
13	7 12	syl6eq	$⊢ (M \in V \land A \in ω \land B \in ω) \to M {Sat}_{\in} ((A \in_{𝑔} B) ⊼_{𝑔} (B \in_{𝑔} A)) = M^{ω}$
14		ovex	$⊢ (A \in_{𝑔} B) ⊼_{𝑔} (B \in_{𝑔} A) \in V$
15		prv	$⊢ (M \in V \land (A \in_{𝑔} B) ⊼_{𝑔} (B \in_{𝑔} A) \in V) \to (M ⊧ ((A \in_{𝑔} B) ⊼_{𝑔} (B \in_{𝑔} A)) \leftrightarrow M {Sat}_{\in} ((A \in_{𝑔} B) ⊼_{𝑔} (B \in_{𝑔} A)) = M^{ω})$
16	1 14 15	sylancl	$⊢ (M \in V \land A \in ω \land B \in ω) \to (M ⊧ ((A \in_{𝑔} B) ⊼_{𝑔} (B \in_{𝑔} A)) \leftrightarrow M {Sat}_{\in} ((A \in_{𝑔} B) ⊼_{𝑔} (B \in_{𝑔} A)) = M^{ω})$
17	13 16	mpbird	$⊢ (M \in V \land A \in ω \land B \in ω) \to M ⊧ ((A \in_{𝑔} B) ⊼_{𝑔} (B \in_{𝑔} A))$