Step 
Hyp 
Ref 
Expression 
1 

mrieqvd.1 
 ( ph > A e. ( Moore ` X ) ) 
2 

mrieqvd.2 
 N = ( mrCls ` A ) 
3 

mrieqvd.3 
 I = ( mrInd ` A ) 
4 

mrieqvd.4 
 ( ph > S C_ X ) 
5 
2 3 1 4

ismri2d 
 ( ph > ( S e. I <> A. x e. S . x e. ( N ` ( S \ { x } ) ) ) ) 
6 
1

adantr 
 ( ( ph /\ x e. S ) > A e. ( Moore ` X ) ) 
7 
4

adantr 
 ( ( ph /\ x e. S ) > S C_ X ) 
8 

simpr 
 ( ( ph /\ x e. S ) > x e. S ) 
9 
6 2 7 8

mrieqvlemd 
 ( ( ph /\ x e. S ) > ( x e. ( N ` ( S \ { x } ) ) <> ( N ` ( S \ { x } ) ) = ( N ` S ) ) ) 
10 
9

necon3bbid 
 ( ( ph /\ x e. S ) > ( . x e. ( N ` ( S \ { x } ) ) <> ( N ` ( S \ { x } ) ) =/= ( N ` S ) ) ) 
11 
10

ralbidva 
 ( ph > ( A. x e. S . x e. ( N ` ( S \ { x } ) ) <> A. x e. S ( N ` ( S \ { x } ) ) =/= ( N ` S ) ) ) 
12 
5 11

bitrd 
 ( ph > ( S e. I <> A. x e. S ( N ` ( S \ { x } ) ) =/= ( N ` S ) ) ) 