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 ∈ Plig → ∅ ∉ G

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ G = ⋃ G
2 1 l2p ⊢ G ∈ Plig ∧ ∅ ∈ G → ∃ a ∈ ⋃ G ∃ b ∈ ⋃ G a ≠ b ∧ a ∈ ∅ ∧ b ∈ ∅
3 noel ⊢ ¬ a ∈ ∅
4 3 pm2.21i ⊢ a ∈ ∅ → ∅ ∉ G
5 4 3ad2ant2 ⊢ a ≠ b ∧ a ∈ ∅ ∧ b ∈ ∅ → ∅ ∉ G
6 5 a1i ⊢ a ∈ ⋃ G ∧ b ∈ ⋃ G → a ≠ b ∧ a ∈ ∅ ∧ b ∈ ∅ → ∅ ∉ G
7 6 rexlimivv ⊢ ∃ a ∈ ⋃ G ∃ b ∈ ⋃ G a ≠ b ∧ a ∈ ∅ ∧ b ∈ ∅ → ∅ ∉ G
8 2 7 syl ⊢ G ∈ Plig ∧ ∅ ∈ G → ∅ ∉ G
9 simpr ⊢ G ∈ Plig ∧ ∅ ∉ G → ∅ ∉ G
10 8 9 pm2.61danel ⊢ G ∈ Plig → ∅ ∉ G