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 e. V /\ A e. _om /\ B e. _om ) -> M |= ( ( A e.g B ) |g ( B e.g A ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	|- ( ( M e. V /\ A e. _om /\ B e. _om ) -> M e. V )
2		3simpc	|- ( ( M e. V /\ A e. _om /\ B e. _om ) -> ( A e. _om /\ B e. _om ) )
3		pm3.22	|- ( ( A e. _om /\ B e. _om ) -> ( B e. _om /\ A e. _om ) )
4	3	3adant1	|- ( ( M e. V /\ A e. _om /\ B e. _om ) -> ( B e. _om /\ A e. _om ) )
5		eqid	|- ( ( A e.g B ) |g ( B e.g A ) ) = ( ( A e.g B ) |g ( B e.g A ) )
6	5	satefvfmla1	|- ( ( M e. V /\ ( A e. _om /\ B e. _om ) /\ ( B e. _om /\ A e. _om ) ) -> ( M SatE ( ( A e.g B ) |g ( B e.g A ) ) ) = { a e. ( M ^m _om ) | ( -. ( a ` A ) e. ( a ` B ) \/ -. ( a ` B ) e. ( a ` A ) ) } )
7	1 2 4 6	syl3anc	|- ( ( M e. V /\ A e. _om /\ B e. _om ) -> ( M SatE ( ( A e.g B ) |g ( B e.g A ) ) ) = { a e. ( M ^m _om ) | ( -. ( a ` A ) e. ( a ` B ) \/ -. ( a ` B ) e. ( a ` A ) ) } )
8		elnanel	|- ( ( a ` A ) e. ( a ` B ) -/\ ( a ` B ) e. ( a ` A ) )
9		nanor	|- ( ( ( a ` A ) e. ( a ` B ) -/\ ( a ` B ) e. ( a ` A ) ) <-> ( -. ( a ` A ) e. ( a ` B ) \/ -. ( a ` B ) e. ( a ` A ) ) )
10	8 9	mpbi	|- ( -. ( a ` A ) e. ( a ` B ) \/ -. ( a ` B ) e. ( a ` A ) )
11	10	a1i	|- ( a e. ( M ^m _om ) -> ( -. ( a ` A ) e. ( a ` B ) \/ -. ( a ` B ) e. ( a ` A ) ) )
12	11	rabeqc	|- { a e. ( M ^m _om ) | ( -. ( a ` A ) e. ( a ` B ) \/ -. ( a ` B ) e. ( a ` A ) ) } = ( M ^m _om )
13	7 12	eqtrdi	|- ( ( M e. V /\ A e. _om /\ B e. _om ) -> ( M SatE ( ( A e.g B ) |g ( B e.g A ) ) ) = ( M ^m _om ) )
14		ovex	|- ( ( A e.g B ) |g ( B e.g A ) ) e. _V
15		prv	|- ( ( M e. V /\ ( ( A e.g B ) |g ( B e.g A ) ) e. _V ) -> ( M |= ( ( A e.g B ) |g ( B e.g A ) ) <-> ( M SatE ( ( A e.g B ) |g ( B e.g A ) ) ) = ( M ^m _om ) ) )
16	1 14 15	sylancl	|- ( ( M e. V /\ A e. _om /\ B e. _om ) -> ( M |= ( ( A e.g B ) |g ( B e.g A ) ) <-> ( M SatE ( ( A e.g B ) |g ( B e.g A ) ) ) = ( M ^m _om ) ) )
17	13 16	mpbird	|- ( ( M e. V /\ A e. _om /\ B e. _om ) -> M |= ( ( A e.g B ) |g ( B e.g A ) ) )