This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem kmlem4

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

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

Proof

Step Hyp Ref Expression
1 elequ1 
 |-  ( v = w -> ( v e. x <-> w e. x ) )
2 neeq2 
 |-  ( v = w -> ( z =/= v <-> z =/= w ) )
3 1 2 anbi12d 
 |-  ( v = w -> ( ( v e. x /\ z =/= v ) <-> ( w e. x /\ z =/= w ) ) )
4 elequ2 
 |-  ( v = w -> ( y e. v <-> y e. w ) )
5 4 notbid 
 |-  ( v = w -> ( -. y e. v <-> -. y e. w ) )
6 3 5 imbi12d 
 |-  ( v = w -> ( ( ( v e. x /\ z =/= v ) -> -. y e. v ) <-> ( ( w e. x /\ z =/= w ) -> -. y e. w ) ) )
7 6 spvv 
 |-  ( A. v ( ( v e. x /\ z =/= v ) -> -. y e. v ) -> ( ( w e. x /\ z =/= w ) -> -. y e. w ) )
8 eldif 
 |-  ( y e. ( z \ U. ( x \ { z } ) ) <-> ( y e. z /\ -. y e. U. ( x \ { z } ) ) )
9 simpr 
 |-  ( ( y e. z /\ -. y e. U. ( x \ { z } ) ) -> -. y e. U. ( x \ { z } ) )
10 eluni 
 |-  ( y e. U. ( x \ { z } ) <-> E. v ( y e. v /\ v e. ( x \ { z } ) ) )
11 10 notbii 
 |-  ( -. y e. U. ( x \ { z } ) <-> -. E. v ( y e. v /\ v e. ( x \ { z } ) ) )
12 alnex 
 |-  ( A. v -. ( y e. v /\ v e. ( x \ { z } ) ) <-> -. E. v ( y e. v /\ v e. ( x \ { z } ) ) )
13 con2b 
 |-  ( ( y e. v -> -. v e. ( x \ { z } ) ) <-> ( v e. ( x \ { z } ) -> -. y e. v ) )
14 imnan 
 |-  ( ( y e. v -> -. v e. ( x \ { z } ) ) <-> -. ( y e. v /\ v e. ( x \ { z } ) ) )
15 eldifsn 
 |-  ( v e. ( x \ { z } ) <-> ( v e. x /\ v =/= z ) )
16 necom 
 |-  ( v =/= z <-> z =/= v )
17 16 anbi2i 
 |-  ( ( v e. x /\ v =/= z ) <-> ( v e. x /\ z =/= v ) )
18 15 17 bitri 
 |-  ( v e. ( x \ { z } ) <-> ( v e. x /\ z =/= v ) )
19 18 imbi1i 
 |-  ( ( v e. ( x \ { z } ) -> -. y e. v ) <-> ( ( v e. x /\ z =/= v ) -> -. y e. v ) )
20 13 14 19 3bitr3i 
 |-  ( -. ( y e. v /\ v e. ( x \ { z } ) ) <-> ( ( v e. x /\ z =/= v ) -> -. y e. v ) )
21 20 albii 
 |-  ( A. v -. ( y e. v /\ v e. ( x \ { z } ) ) <-> A. v ( ( v e. x /\ z =/= v ) -> -. y e. v ) )
22 11 12 21 3bitr2i 
 |-  ( -. y e. U. ( x \ { z } ) <-> A. v ( ( v e. x /\ z =/= v ) -> -. y e. v ) )
23 9 22 sylib 
 |-  ( ( y e. z /\ -. y e. U. ( x \ { z } ) ) -> A. v ( ( v e. x /\ z =/= v ) -> -. y e. v ) )
24 8 23 sylbi 
 |-  ( y e. ( z \ U. ( x \ { z } ) ) -> A. v ( ( v e. x /\ z =/= v ) -> -. y e. v ) )
25 7 24 syl11 
 |-  ( ( w e. x /\ z =/= w ) -> ( y e. ( z \ U. ( x \ { z } ) ) -> -. y e. w ) )
26 25 ralrimiv 
 |-  ( ( w e. x /\ z =/= w ) -> A. y e. ( z \ U. ( x \ { z } ) ) -. y e. w )
27 disj 
 |-  ( ( ( z \ U. ( x \ { z } ) ) i^i w ) = (/) <-> A. y e. ( z \ U. ( x \ { z } ) ) -. y e. w )
28 26 27 sylibr 
 |-  ( ( w e. x /\ z =/= w ) -> ( ( z \ U. ( x \ { z } ) ) i^i w ) = (/) )