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

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