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