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 eluni 
 |-  ( y e. U. ( x \ { z } ) <-> E. v ( y e. v /\ v e. ( x \ { z } ) ) )
10 9 notbii 
 |-  ( -. y e. U. ( x \ { z } ) <-> -. E. v ( y e. v /\ v e. ( x \ { z } ) ) )
11 alnex 
 |-  ( A. v -. ( y e. v /\ v e. ( x \ { z } ) ) <-> -. E. v ( y e. v /\ v e. ( x \ { z } ) ) )
12 con2b 
 |-  ( ( y e. v -> -. v e. ( x \ { z } ) ) <-> ( v e. ( x \ { z } ) -> -. y e. v ) )
13 imnan 
 |-  ( ( y e. v -> -. v e. ( x \ { z } ) ) <-> -. ( y e. v /\ v e. ( x \ { z } ) ) )
14 eldifsn 
 |-  ( v e. ( x \ { z } ) <-> ( v e. x /\ v =/= z ) )
15 necom 
 |-  ( v =/= z <-> z =/= v )
16 15 anbi2i 
 |-  ( ( v e. x /\ v =/= z ) <-> ( v e. x /\ z =/= v ) )
17 14 16 bitri 
 |-  ( v e. ( x \ { z } ) <-> ( v e. x /\ z =/= v ) )
18 17 imbi1i 
 |-  ( ( v e. ( x \ { z } ) -> -. y e. v ) <-> ( ( v e. x /\ z =/= v ) -> -. y e. v ) )
19 12 13 18 3bitr3i 
 |-  ( -. ( y e. v /\ v e. ( x \ { z } ) ) <-> ( ( v e. x /\ z =/= v ) -> -. y e. v ) )
20 19 albii 
 |-  ( A. v -. ( y e. v /\ v e. ( x \ { z } ) ) <-> A. v ( ( v e. x /\ z =/= v ) -> -. y e. v ) )
21 10 11 20 3bitr2i 
 |-  ( -. y e. U. ( x \ { z } ) <-> A. v ( ( v e. x /\ z =/= v ) -> -. y e. v ) )
22 21 bilani 
 |-  ( ( y e. z /\ -. y e. U. ( x \ { z } ) ) -> A. v ( ( v e. x /\ z =/= v ) -> -. y e. v ) )
23 8 22 sylbi 
 |-  ( y e. ( z \ U. ( x \ { z } ) ) -> A. v ( ( v e. x /\ z =/= v ) -> -. y e. v ) )
24 7 23 syl11 
 |-  ( ( w e. x /\ z =/= w ) -> ( y e. ( z \ U. ( x \ { z } ) ) -> -. y e. w ) )
25 24 ralrimiv 
 |-  ( ( w e. x /\ z =/= w ) -> A. y e. ( z \ U. ( x \ { z } ) ) -. y e. w )
26 disj 
 |-  ( ( ( z \ U. ( x \ { z } ) ) i^i w ) = (/) <-> A. y e. ( z \ U. ( x \ { z } ) ) -. y e. w )
27 25 26 sylibr 
 |-  ( ( w e. x /\ z =/= w ) -> ( ( z \ U. ( x \ { z } ) ) i^i w ) = (/) )