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 ) = (/) )