Theorem nsnlpligALT

Description: Alternate version of nsnlplig using the predicate e/ instead of -. e. and whose proof is shorter. (Contributed by AV, 5-Dec-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	nsnlpligALT	$$⊢G\in \mathrm{Plig}\to \left\{A\right\}\notin G$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup G=\bigcup G$$
2	1	l2p	$$⊢\left(G\in \mathrm{Plig}\wedge \left\{A\right\}\in G\right)\to \exists a\in \bigcup G\exists b\in \bigcup G\left(a\ne b\wedge a\in \left\{A\right\}\wedge b\in \left\{A\right\}\right)$$
3		elsni	$$⊢a\in \left\{A\right\}\to a=A$$
4		elsni	$$⊢b\in \left\{A\right\}\to b=A$$
5		eqtr3	$$⊢\left(a=A\wedge b=A\right)\to a=b$$
6		eqneqall	$$⊢a=b\to \left(a\ne b\to \left\{A\right\}\notin G\right)$$
7	5 6	syl	$$⊢\left(a=A\wedge b=A\right)\to \left(a\ne b\to \left\{A\right\}\notin G\right)$$
8	3 4 7	syl2an	$$⊢\left(a\in \left\{A\right\}\wedge b\in \left\{A\right\}\right)\to \left(a\ne b\to \left\{A\right\}\notin G\right)$$
9	8	impcom	$$⊢\left(a\ne b\wedge \left(a\in \left\{A\right\}\wedge b\in \left\{A\right\}\right)\right)\to \left\{A\right\}\notin G$$
10	9	3impb	$$⊢\left(a\ne b\wedge a\in \left\{A\right\}\wedge b\in \left\{A\right\}\right)\to \left\{A\right\}\notin G$$
11	10	a1i	$$⊢\left(a\in \bigcup G\wedge b\in \bigcup G\right)\to \left(\left(a\ne b\wedge a\in \left\{A\right\}\wedge b\in \left\{A\right\}\right)\to \left\{A\right\}\notin G\right)$$
12	11	rexlimivv	$$⊢\exists a\in \bigcup G\exists b\in \bigcup G\left(a\ne b\wedge a\in \left\{A\right\}\wedge b\in \left\{A\right\}\right)\to \left\{A\right\}\notin G$$
13	2 12	syl	$$⊢\left(G\in \mathrm{Plig}\wedge \left\{A\right\}\in G\right)\to \left\{A\right\}\notin G$$
14		simpr	$$⊢\left(G\in \mathrm{Plig}\wedge \left\{A\right\}\notin G\right)\to \left\{A\right\}\notin G$$
15	13 14	pm2.61danel	$$⊢G\in \mathrm{Plig}\to \left\{A\right\}\notin G$$