This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V ∧ A ∈ ω ∧ B ∈ ω → M ⊧ A ∈ 𝑔 B ⊼ 𝑔 B ∈ 𝑔 A

Proof

Step Hyp Ref Expression
1 simp1 ⊢ M ∈ V ∧ A ∈ ω ∧ B ∈ ω → M ∈ V
2 3simpc ⊢ M ∈ V ∧ A ∈ ω ∧ B ∈ ω → A ∈ ω ∧ B ∈ ω
3 pm3.22 ⊢ A ∈ ω ∧ B ∈ ω → B ∈ ω ∧ A ∈ ω
4 3 3adant1 ⊢ M ∈ V ∧ A ∈ ω ∧ B ∈ ω → B ∈ ω ∧ A ∈ ω
5 eqid ⊢ A ∈ 𝑔 B ⊼ 𝑔 B ∈ 𝑔 A = A ∈ 𝑔 B ⊼ 𝑔 B ∈ 𝑔 A
6 5 satefvfmla1 ⊢ M ∈ V ∧ A ∈ ω ∧ B ∈ ω ∧ B ∈ ω ∧ A ∈ ω → M Sat ∈ A ∈ 𝑔 B ⊼ 𝑔 B ∈ 𝑔 A = a ∈ M ω | ¬ a ⁡ A ∈ a ⁡ B ∨ ¬ a ⁡ B ∈ a ⁡ A
7 1 2 4 6 syl3anc ⊢ M ∈ V ∧ A ∈ ω ∧ B ∈ ω → M Sat ∈ A ∈ 𝑔 B ⊼ 𝑔 B ∈ 𝑔 A = a ∈ M ω | ¬ a ⁡ A ∈ a ⁡ B ∨ ¬ a ⁡ B ∈ a ⁡ A
8 elnanel ⊢ a ⁡ A ∈ a ⁡ B ⊼ a ⁡ B ∈ a ⁡ A
9 nanor ⊢ a ⁡ A ∈ a ⁡ B ⊼ a ⁡ B ∈ a ⁡ A ↔ ¬ a ⁡ A ∈ a ⁡ B ∨ ¬ a ⁡ B ∈ a ⁡ A
10 8 9 mpbi ⊢ ¬ a ⁡ A ∈ a ⁡ B ∨ ¬ a ⁡ B ∈ a ⁡ A
11 10 a1i ⊢ a ∈ M ω → ¬ a ⁡ A ∈ a ⁡ B ∨ ¬ a ⁡ B ∈ a ⁡ A
12 11 rabeqc ⊢ a ∈ M ω | ¬ a ⁡ A ∈ a ⁡ B ∨ ¬ a ⁡ B ∈ a ⁡ A = M ω
13 7 12 eqtrdi ⊢ M ∈ V ∧ A ∈ ω ∧ B ∈ ω → M Sat ∈ A ∈ 𝑔 B ⊼ 𝑔 B ∈ 𝑔 A = M ω
14 ovex ⊢ A ∈ 𝑔 B ⊼ 𝑔 B ∈ 𝑔 A ∈ V
15 prv ⊢ M ∈ V ∧ A ∈ 𝑔 B ⊼ 𝑔 B ∈ 𝑔 A ∈ V → M ⊧ A ∈ 𝑔 B ⊼ 𝑔 B ∈ 𝑔 A ↔ M Sat ∈ A ∈ 𝑔 B ⊼ 𝑔 B ∈ 𝑔 A = M ω
16 1 14 15 sylancl ⊢ M ∈ V ∧ A ∈ ω ∧ B ∈ ω → M ⊧ A ∈ 𝑔 B ⊼ 𝑔 B ∈ 𝑔 A ↔ M Sat ∈ A ∈ 𝑔 B ⊼ 𝑔 B ∈ 𝑔 A = M ω
17 13 16 mpbird ⊢ M ∈ V ∧ A ∈ ω ∧ B ∈ ω → M ⊧ A ∈ 𝑔 B ⊼ 𝑔 B ∈ 𝑔 A