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 ) ) )