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 e. Plig -> (/) e/ G )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. G = U. G
2 1 l2p 
 |-  ( ( G e. Plig /\ (/) e. G ) -> E. a e. U. G E. b e. U. G ( a =/= b /\ a e. (/) /\ b e. (/) ) )
3 noel 
 |-  -. a e. (/)
4 3 pm2.21i 
 |-  ( a e. (/) -> (/) e/ G )
5 4 3ad2ant2 
 |-  ( ( a =/= b /\ a e. (/) /\ b e. (/) ) -> (/) e/ G )
6 5 a1i 
 |-  ( ( a e. U. G /\ b e. U. G ) -> ( ( a =/= b /\ a e. (/) /\ b e. (/) ) -> (/) e/ G ) )
7 6 rexlimivv 
 |-  ( E. a e. U. G E. b e. U. G ( a =/= b /\ a e. (/) /\ b e. (/) ) -> (/) e/ G )
8 2 7 syl 
 |-  ( ( G e. Plig /\ (/) e. G ) -> (/) e/ G )
9 simpr 
 |-  ( ( G e. Plig /\ (/) e/ G ) -> (/) e/ G )
10 8 9 pm2.61danel 
 |-  ( G e. Plig -> (/) e/ G )