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	⊢ ( 𝐺 ∈ Plig → ∅ ∉ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐺 = ∪ 𝐺
2	1	l2p	⊢ ( ( 𝐺 ∈ Plig ∧ ∅ ∈ 𝐺 ) → ∃ 𝑎 ∈ ∪ 𝐺 ∃ 𝑏 ∈ ∪ 𝐺 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ ∅ ∧ 𝑏 ∈ ∅ ) )
3		noel	⊢ ¬ 𝑎 ∈ ∅
4	3	pm2.21i	⊢ ( 𝑎 ∈ ∅ → ∅ ∉ 𝐺 )
5	4	3ad2ant2	⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ ∅ ∧ 𝑏 ∈ ∅ ) → ∅ ∉ 𝐺 )
6	5	a1i	⊢ ( ( 𝑎 ∈ ∪ 𝐺 ∧ 𝑏 ∈ ∪ 𝐺 ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ ∅ ∧ 𝑏 ∈ ∅ ) → ∅ ∉ 𝐺 ) )
7	6	rexlimivv	⊢ ( ∃ 𝑎 ∈ ∪ 𝐺 ∃ 𝑏 ∈ ∪ 𝐺 ( 𝑎 ≠ 𝑏 ∧ 𝑎 ∈ ∅ ∧ 𝑏 ∈ ∅ ) → ∅ ∉ 𝐺 )
8	2 7	syl	⊢ ( ( 𝐺 ∈ Plig ∧ ∅ ∈ 𝐺 ) → ∅ ∉ 𝐺 )
9		simpr	⊢ ( ( 𝐺 ∈ Plig ∧ ∅ ∉ 𝐺 ) → ∅ ∉ 𝐺 )
10	8 9	pm2.61danel	⊢ ( 𝐺 ∈ Plig → ∅ ∉ 𝐺 )