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 ( 𝐺 ∈ Plig → { 𝐴 } ∉ 𝐺 )

Proof

Step Hyp Ref Expression
1 eqid 𝐺 = 𝐺
2 1 l2p ( ( 𝐺 ∈ Plig ∧ { 𝐴 } ∈ 𝐺 ) → ∃ 𝑎 𝐺𝑏 𝐺 ( 𝑎𝑏𝑎 ∈ { 𝐴 } ∧ 𝑏 ∈ { 𝐴 } ) )
3 elsni ( 𝑎 ∈ { 𝐴 } → 𝑎 = 𝐴 )
4 elsni ( 𝑏 ∈ { 𝐴 } → 𝑏 = 𝐴 )
5 eqtr3 ( ( 𝑎 = 𝐴𝑏 = 𝐴 ) → 𝑎 = 𝑏 )
6 eqneqall ( 𝑎 = 𝑏 → ( 𝑎𝑏 → { 𝐴 } ∉ 𝐺 ) )
7 5 6 syl ( ( 𝑎 = 𝐴𝑏 = 𝐴 ) → ( 𝑎𝑏 → { 𝐴 } ∉ 𝐺 ) )
8 3 4 7 syl2an ( ( 𝑎 ∈ { 𝐴 } ∧ 𝑏 ∈ { 𝐴 } ) → ( 𝑎𝑏 → { 𝐴 } ∉ 𝐺 ) )
9 8 impcom ( ( 𝑎𝑏 ∧ ( 𝑎 ∈ { 𝐴 } ∧ 𝑏 ∈ { 𝐴 } ) ) → { 𝐴 } ∉ 𝐺 )
10 9 3impb ( ( 𝑎𝑏𝑎 ∈ { 𝐴 } ∧ 𝑏 ∈ { 𝐴 } ) → { 𝐴 } ∉ 𝐺 )
11 10 a1i ( ( 𝑎 𝐺𝑏 𝐺 ) → ( ( 𝑎𝑏𝑎 ∈ { 𝐴 } ∧ 𝑏 ∈ { 𝐴 } ) → { 𝐴 } ∉ 𝐺 ) )
12 11 rexlimivv ( ∃ 𝑎 𝐺𝑏 𝐺 ( 𝑎𝑏𝑎 ∈ { 𝐴 } ∧ 𝑏 ∈ { 𝐴 } ) → { 𝐴 } ∉ 𝐺 )
13 2 12 syl ( ( 𝐺 ∈ Plig ∧ { 𝐴 } ∈ 𝐺 ) → { 𝐴 } ∉ 𝐺 )
14 simpr ( ( 𝐺 ∈ Plig ∧ { 𝐴 } ∉ 𝐺 ) → { 𝐴 } ∉ 𝐺 )
15 13 14 pm2.61danel ( 𝐺 ∈ Plig → { 𝐴 } ∉ 𝐺 )