# Metamath Proof Explorer

## Theorem n0lpligALT

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

Ref Expression
Assertion n0lpligALT ${⊢}{G}\in \mathrm{Plig}\to \varnothing \notin {G}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\bigcup {G}=\bigcup {G}$
2 1 l2p ${⊢}\left({G}\in \mathrm{Plig}\wedge \varnothing \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 \varnothing \wedge {b}\in \varnothing \right)$
3 noel ${⊢}¬{a}\in \varnothing$
4 3 pm2.21i ${⊢}{a}\in \varnothing \to \varnothing \notin {G}$
5 4 3ad2ant2 ${⊢}\left({a}\ne {b}\wedge {a}\in \varnothing \wedge {b}\in \varnothing \right)\to \varnothing \notin {G}$
6 5 a1i ${⊢}\left({a}\in \bigcup {G}\wedge {b}\in \bigcup {G}\right)\to \left(\left({a}\ne {b}\wedge {a}\in \varnothing \wedge {b}\in \varnothing \right)\to \varnothing \notin {G}\right)$
7 6 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 \varnothing \wedge {b}\in \varnothing \right)\to \varnothing \notin {G}$
8 2 7 syl ${⊢}\left({G}\in \mathrm{Plig}\wedge \varnothing \in {G}\right)\to \varnothing \notin {G}$
9 simpr ${⊢}\left({G}\in \mathrm{Plig}\wedge \varnothing \notin {G}\right)\to \varnothing \notin {G}$
10 8 9 pm2.61danel ${⊢}{G}\in \mathrm{Plig}\to \varnothing \notin {G}$