Metamath Proof Explorer

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}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {G}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\exists {b}\in \bigcup {G}\phantom{\rule{.4em}{0ex}}\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}$