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

Metamath Proof Explorer

Theorem kmlem3

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. The right-hand side is part of the hypothesis of 4. (Contributed by NM, 25-Mar-2004)

Ref Expression
Assertion kmlem3 
|- ( ( z \ U. ( x \ { z } ) ) =/= (/) <-> E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) )

Proof

Step Hyp Ref Expression
1 dfdif2 
 |-  ( z \ U. ( x \ { z } ) ) = { v e. z | -. v e. U. ( x \ { z } ) }
2 dfnul3 
 |-  (/) = { v e. z | -. v e. z }
3 2 uneq2i 
 |-  ( { v e. z | -. v e. U. ( x \ { z } ) } u. (/) ) = ( { v e. z | -. v e. U. ( x \ { z } ) } u. { v e. z | -. v e. z } )
4 un0 
 |-  ( { v e. z | -. v e. U. ( x \ { z } ) } u. (/) ) = { v e. z | -. v e. U. ( x \ { z } ) }
5 unrab 
 |-  ( { v e. z | -. v e. U. ( x \ { z } ) } u. { v e. z | -. v e. z } ) = { v e. z | ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) }
6 3 4 5 3eqtr3i 
 |-  { v e. z | -. v e. U. ( x \ { z } ) } = { v e. z | ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) }
7 ianor 
 |-  ( -. ( v e. U. ( x \ { z } ) /\ v e. z ) <-> ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) )
8 eluni 
 |-  ( v e. U. ( x \ { z } ) <-> E. w ( v e. w /\ w e. ( x \ { z } ) ) )
9 8 anbi1i 
 |-  ( ( v e. U. ( x \ { z } ) /\ v e. z ) <-> ( E. w ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) )
10 df-rex 
 |-  ( E. w e. x -. ( z =/= w -> -. v e. ( z i^i w ) ) <-> E. w ( w e. x /\ -. ( z =/= w -> -. v e. ( z i^i w ) ) ) )
11 elin 
 |-  ( v e. ( z i^i w ) <-> ( v e. z /\ v e. w ) )
12 11 anbi2i 
 |-  ( ( z =/= w /\ v e. ( z i^i w ) ) <-> ( z =/= w /\ ( v e. z /\ v e. w ) ) )
13 df-an 
 |-  ( ( z =/= w /\ v e. ( z i^i w ) ) <-> -. ( z =/= w -> -. v e. ( z i^i w ) ) )
14 12 13 bitr3i 
 |-  ( ( z =/= w /\ ( v e. z /\ v e. w ) ) <-> -. ( z =/= w -> -. v e. ( z i^i w ) ) )
15 14 anbi2i 
 |-  ( ( w e. x /\ ( z =/= w /\ ( v e. z /\ v e. w ) ) ) <-> ( w e. x /\ -. ( z =/= w -> -. v e. ( z i^i w ) ) ) )
16 eldifsn 
 |-  ( w e. ( x \ { z } ) <-> ( w e. x /\ w =/= z ) )
17 necom 
 |-  ( w =/= z <-> z =/= w )
18 17 anbi2i 
 |-  ( ( w e. x /\ w =/= z ) <-> ( w e. x /\ z =/= w ) )
19 16 18 bitri 
 |-  ( w e. ( x \ { z } ) <-> ( w e. x /\ z =/= w ) )
20 19 anbi2i 
 |-  ( ( ( v e. w /\ v e. z ) /\ w e. ( x \ { z } ) ) <-> ( ( v e. w /\ v e. z ) /\ ( w e. x /\ z =/= w ) ) )
21 ancom 
 |-  ( ( v e. w /\ v e. z ) <-> ( v e. z /\ v e. w ) )
22 21 anbi2ci 
 |-  ( ( ( v e. w /\ v e. z ) /\ ( w e. x /\ z =/= w ) ) <-> ( ( w e. x /\ z =/= w ) /\ ( v e. z /\ v e. w ) ) )
23 anass 
 |-  ( ( ( w e. x /\ z =/= w ) /\ ( v e. z /\ v e. w ) ) <-> ( w e. x /\ ( z =/= w /\ ( v e. z /\ v e. w ) ) ) )
24 20 22 23 3bitri 
 |-  ( ( ( v e. w /\ v e. z ) /\ w e. ( x \ { z } ) ) <-> ( w e. x /\ ( z =/= w /\ ( v e. z /\ v e. w ) ) ) )
25 an32 
 |-  ( ( ( v e. w /\ v e. z ) /\ w e. ( x \ { z } ) ) <-> ( ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) )
26 24 25 bitr3i 
 |-  ( ( w e. x /\ ( z =/= w /\ ( v e. z /\ v e. w ) ) ) <-> ( ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) )
27 15 26 bitr3i 
 |-  ( ( w e. x /\ -. ( z =/= w -> -. v e. ( z i^i w ) ) ) <-> ( ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) )
28 27 exbii 
 |-  ( E. w ( w e. x /\ -. ( z =/= w -> -. v e. ( z i^i w ) ) ) <-> E. w ( ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) )
29 19.41v 
 |-  ( E. w ( ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) <-> ( E. w ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) )
30 10 28 29 3bitri 
 |-  ( E. w e. x -. ( z =/= w -> -. v e. ( z i^i w ) ) <-> ( E. w ( v e. w /\ w e. ( x \ { z } ) ) /\ v e. z ) )
31 rexnal 
 |-  ( E. w e. x -. ( z =/= w -> -. v e. ( z i^i w ) ) <-> -. A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) )
32 9 30 31 3bitr2ri 
 |-  ( -. A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) <-> ( v e. U. ( x \ { z } ) /\ v e. z ) )
33 32 con1bii 
 |-  ( -. ( v e. U. ( x \ { z } ) /\ v e. z ) <-> A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) )
34 7 33 bitr3i 
 |-  ( ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) <-> A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) )
35 34 rabbii 
 |-  { v e. z | ( -. v e. U. ( x \ { z } ) \/ -. v e. z ) } = { v e. z | A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) }
36 1 6 35 3eqtri 
 |-  ( z \ U. ( x \ { z } ) ) = { v e. z | A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) }
37 36 neeq1i 
 |-  ( ( z \ U. ( x \ { z } ) ) =/= (/) <-> { v e. z | A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) } =/= (/) )
38 rabn0 
 |-  ( { v e. z | A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) } =/= (/) <-> E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) )
39 37 38 bitri 
 |-  ( ( z \ U. ( x \ { z } ) ) =/= (/) <-> E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) )