Metamath Proof Explorer

Theorem kmlem5

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004)

Ref Expression
Assertion kmlem5 
|- ( ( w e. x /\ z =/= w ) -> ( ( z \ U. ( x \ { z } ) ) i^i ( w \ U. ( x \ { w } ) ) ) = (/) )

Proof

Step Hyp Ref Expression
1 difss 
 |-  ( w \ U. ( x \ { w } ) ) C_ w
2 sslin 
 |-  ( ( w \ U. ( x \ { w } ) ) C_ w -> ( ( z \ U. ( x \ { z } ) ) i^i ( w \ U. ( x \ { w } ) ) ) C_ ( ( z \ U. ( x \ { z } ) ) i^i w ) )
3 1 2 ax-mp 
 |-  ( ( z \ U. ( x \ { z } ) ) i^i ( w \ U. ( x \ { w } ) ) ) C_ ( ( z \ U. ( x \ { z } ) ) i^i w )
4 kmlem4 
 |-  ( ( w e. x /\ z =/= w ) -> ( ( z \ U. ( x \ { z } ) ) i^i w ) = (/) )
5 3 4 sseqtrid 
 |-  ( ( w e. x /\ z =/= w ) -> ( ( z \ U. ( x \ { z } ) ) i^i ( w \ U. ( x \ { w } ) ) ) C_ (/) )
6 ss0b 
 |-  ( ( ( z \ U. ( x \ { z } ) ) i^i ( w \ U. ( x \ { w } ) ) ) C_ (/) <-> ( ( z \ U. ( x \ { z } ) ) i^i ( w \ U. ( x \ { w } ) ) ) = (/) )
7 5 6 sylib 
 |-  ( ( w e. x /\ z =/= w ) -> ( ( z \ U. ( x \ { z } ) ) i^i ( w \ U. ( x \ { w } ) ) ) = (/) )