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