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 ( ( 𝑀𝑉𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → 𝑀 ⊧ ( ( 𝐴𝑔 𝐵 ) ⊼𝑔 ( 𝐵𝑔 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ( ( 𝑀𝑉𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → 𝑀𝑉 )
2 3simpc ( ( 𝑀𝑉𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) )
3 pm3.22 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) )
4 3 3adant1 ( ( 𝑀𝑉𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) )
5 eqid ( ( 𝐴𝑔 𝐵 ) ⊼𝑔 ( 𝐵𝑔 𝐴 ) ) = ( ( 𝐴𝑔 𝐵 ) ⊼𝑔 ( 𝐵𝑔 𝐴 ) )
6 5 satefvfmla1 ( ( 𝑀𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) ) → ( 𝑀 Sat ( ( 𝐴𝑔 𝐵 ) ⊼𝑔 ( 𝐵𝑔 𝐴 ) ) ) = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( ¬ ( 𝑎𝐴 ) ∈ ( 𝑎𝐵 ) ∨ ¬ ( 𝑎𝐵 ) ∈ ( 𝑎𝐴 ) ) } )
7 1 2 4 6 syl3anc ( ( 𝑀𝑉𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝑀 Sat ( ( 𝐴𝑔 𝐵 ) ⊼𝑔 ( 𝐵𝑔 𝐴 ) ) ) = { 𝑎 ∈ ( 𝑀m ω ) ∣ ( ¬ ( 𝑎𝐴 ) ∈ ( 𝑎𝐵 ) ∨ ¬ ( 𝑎𝐵 ) ∈ ( 𝑎𝐴 ) ) } )
8 elnanel ( ( 𝑎𝐴 ) ∈ ( 𝑎𝐵 ) ⊼ ( 𝑎𝐵 ) ∈ ( 𝑎𝐴 ) )
9 nanor ( ( ( 𝑎𝐴 ) ∈ ( 𝑎𝐵 ) ⊼ ( 𝑎𝐵 ) ∈ ( 𝑎𝐴 ) ) ↔ ( ¬ ( 𝑎𝐴 ) ∈ ( 𝑎𝐵 ) ∨ ¬ ( 𝑎𝐵 ) ∈ ( 𝑎𝐴 ) ) )
10 8 9 mpbi ( ¬ ( 𝑎𝐴 ) ∈ ( 𝑎𝐵 ) ∨ ¬ ( 𝑎𝐵 ) ∈ ( 𝑎𝐴 ) )
11 10 a1i ( 𝑎 ∈ ( 𝑀m ω ) → ( ¬ ( 𝑎𝐴 ) ∈ ( 𝑎𝐵 ) ∨ ¬ ( 𝑎𝐵 ) ∈ ( 𝑎𝐴 ) ) )
12 11 rabeqc { 𝑎 ∈ ( 𝑀m ω ) ∣ ( ¬ ( 𝑎𝐴 ) ∈ ( 𝑎𝐵 ) ∨ ¬ ( 𝑎𝐵 ) ∈ ( 𝑎𝐴 ) ) } = ( 𝑀m ω )
13 7 12 eqtrdi ( ( 𝑀𝑉𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝑀 Sat ( ( 𝐴𝑔 𝐵 ) ⊼𝑔 ( 𝐵𝑔 𝐴 ) ) ) = ( 𝑀m ω ) )
14 ovex ( ( 𝐴𝑔 𝐵 ) ⊼𝑔 ( 𝐵𝑔 𝐴 ) ) ∈ V
15 prv ( ( 𝑀𝑉 ∧ ( ( 𝐴𝑔 𝐵 ) ⊼𝑔 ( 𝐵𝑔 𝐴 ) ) ∈ V ) → ( 𝑀 ⊧ ( ( 𝐴𝑔 𝐵 ) ⊼𝑔 ( 𝐵𝑔 𝐴 ) ) ↔ ( 𝑀 Sat ( ( 𝐴𝑔 𝐵 ) ⊼𝑔 ( 𝐵𝑔 𝐴 ) ) ) = ( 𝑀m ω ) ) )
16 1 14 15 sylancl ( ( 𝑀𝑉𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝑀 ⊧ ( ( 𝐴𝑔 𝐵 ) ⊼𝑔 ( 𝐵𝑔 𝐴 ) ) ↔ ( 𝑀 Sat ( ( 𝐴𝑔 𝐵 ) ⊼𝑔 ( 𝐵𝑔 𝐴 ) ) ) = ( 𝑀m ω ) ) )
17 13 16 mpbird ( ( 𝑀𝑉𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → 𝑀 ⊧ ( ( 𝐴𝑔 𝐵 ) ⊼𝑔 ( 𝐵𝑔 𝐴 ) ) )