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