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 Plig \to \emptyset \notin G$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ G = ⋃ G$
2	1	l2p	$⊢ (G \in Plig \land \emptyset \in G) \to \exists a \in ⋃ G \exists b \in ⋃ G (a \neq b \land a \in \emptyset \land b \in \emptyset)$
3		noel	$⊢ \neg a \in \emptyset$
4	3	pm2.21i	$⊢ a \in \emptyset \to \emptyset \notin G$
5	4	3ad2ant2	$⊢ (a \neq b \land a \in \emptyset \land b \in \emptyset) \to \emptyset \notin G$
6	5	a1i	$⊢ (a \in ⋃ G \land b \in ⋃ G) \to ((a \neq b \land a \in \emptyset \land b \in \emptyset) \to \emptyset \notin G)$
7	6	rexlimivv	$⊢ \exists a \in ⋃ G \exists b \in ⋃ G (a \neq b \land a \in \emptyset \land b \in \emptyset) \to \emptyset \notin G$
8	2 7	syl	$⊢ (G \in Plig \land \emptyset \in G) \to \emptyset \notin G$
9		simpr	$⊢ (G \in Plig \land \emptyset \notin G) \to \emptyset \notin G$
10	8 9	pm2.61danel	$⊢ G \in Plig \to \emptyset \notin G$