Metamath Proof Explorer

Theorem kmlem9

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

Ref Expression
Hypothesis kmlem9.1 
|- A = { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) }
Assertion kmlem9 
|- A. z e. A A. w e. A ( z =/= w -> ( z i^i w ) = (/) )

Proof

Step Hyp Ref Expression
1 kmlem9.1 
 |-  A = { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) }
2 vex 
 |-  z e. _V
3 eqeq1 
 |-  ( u = z -> ( u = ( t \ U. ( x \ { t } ) ) <-> z = ( t \ U. ( x \ { t } ) ) ) )
4 3 rexbidv 
 |-  ( u = z -> ( E. t e. x u = ( t \ U. ( x \ { t } ) ) <-> E. t e. x z = ( t \ U. ( x \ { t } ) ) ) )
5 2 4 1 elab2 
 |-  ( z e. A <-> E. t e. x z = ( t \ U. ( x \ { t } ) ) )
6 vex 
 |-  w e. _V
7 eqeq1 
 |-  ( u = w -> ( u = ( t \ U. ( x \ { t } ) ) <-> w = ( t \ U. ( x \ { t } ) ) ) )
8 7 rexbidv 
 |-  ( u = w -> ( E. t e. x u = ( t \ U. ( x \ { t } ) ) <-> E. t e. x w = ( t \ U. ( x \ { t } ) ) ) )
9 6 8 1 elab2 
 |-  ( w e. A <-> E. t e. x w = ( t \ U. ( x \ { t } ) ) )
10 difeq1 
 |-  ( t = h -> ( t \ U. ( x \ { t } ) ) = ( h \ U. ( x \ { t } ) ) )
11 sneq 
 |-  ( t = h -> { t } = { h } )
12 11 difeq2d 
 |-  ( t = h -> ( x \ { t } ) = ( x \ { h } ) )
13 12 unieqd 
 |-  ( t = h -> U. ( x \ { t } ) = U. ( x \ { h } ) )
14 13 difeq2d 
 |-  ( t = h -> ( h \ U. ( x \ { t } ) ) = ( h \ U. ( x \ { h } ) ) )
15 10 14 eqtrd 
 |-  ( t = h -> ( t \ U. ( x \ { t } ) ) = ( h \ U. ( x \ { h } ) ) )
16 15 eqeq2d 
 |-  ( t = h -> ( w = ( t \ U. ( x \ { t } ) ) <-> w = ( h \ U. ( x \ { h } ) ) ) )
17 16 cbvrexvw 
 |-  ( E. t e. x w = ( t \ U. ( x \ { t } ) ) <-> E. h e. x w = ( h \ U. ( x \ { h } ) ) )
18 9 17 bitri 
 |-  ( w e. A <-> E. h e. x w = ( h \ U. ( x \ { h } ) ) )
19 reeanv 
 |-  ( E. t e. x E. h e. x ( z = ( t \ U. ( x \ { t } ) ) /\ w = ( h \ U. ( x \ { h } ) ) ) <-> ( E. t e. x z = ( t \ U. ( x \ { t } ) ) /\ E. h e. x w = ( h \ U. ( x \ { h } ) ) ) )
20 eqeq12 
 |-  ( ( z = ( t \ U. ( x \ { t } ) ) /\ w = ( h \ U. ( x \ { h } ) ) ) -> ( z = w <-> ( t \ U. ( x \ { t } ) ) = ( h \ U. ( x \ { h } ) ) ) )
21 15 20 syl5ibr 
 |-  ( ( z = ( t \ U. ( x \ { t } ) ) /\ w = ( h \ U. ( x \ { h } ) ) ) -> ( t = h -> z = w ) )
22 21 necon3d 
 |-  ( ( z = ( t \ U. ( x \ { t } ) ) /\ w = ( h \ U. ( x \ { h } ) ) ) -> ( z =/= w -> t =/= h ) )
23 kmlem5 
 |-  ( ( h e. x /\ t =/= h ) -> ( ( t \ U. ( x \ { t } ) ) i^i ( h \ U. ( x \ { h } ) ) ) = (/) )
24 ineq12 
 |-  ( ( z = ( t \ U. ( x \ { t } ) ) /\ w = ( h \ U. ( x \ { h } ) ) ) -> ( z i^i w ) = ( ( t \ U. ( x \ { t } ) ) i^i ( h \ U. ( x \ { h } ) ) ) )
25 24 eqeq1d 
 |-  ( ( z = ( t \ U. ( x \ { t } ) ) /\ w = ( h \ U. ( x \ { h } ) ) ) -> ( ( z i^i w ) = (/) <-> ( ( t \ U. ( x \ { t } ) ) i^i ( h \ U. ( x \ { h } ) ) ) = (/) ) )
26 23 25 syl5ibr 
 |-  ( ( z = ( t \ U. ( x \ { t } ) ) /\ w = ( h \ U. ( x \ { h } ) ) ) -> ( ( h e. x /\ t =/= h ) -> ( z i^i w ) = (/) ) )
27 26 expd 
 |-  ( ( z = ( t \ U. ( x \ { t } ) ) /\ w = ( h \ U. ( x \ { h } ) ) ) -> ( h e. x -> ( t =/= h -> ( z i^i w ) = (/) ) ) )
28 22 27 syl5d 
 |-  ( ( z = ( t \ U. ( x \ { t } ) ) /\ w = ( h \ U. ( x \ { h } ) ) ) -> ( h e. x -> ( z =/= w -> ( z i^i w ) = (/) ) ) )
29 28 com12 
 |-  ( h e. x -> ( ( z = ( t \ U. ( x \ { t } ) ) /\ w = ( h \ U. ( x \ { h } ) ) ) -> ( z =/= w -> ( z i^i w ) = (/) ) ) )
30 29 adantl 
 |-  ( ( t e. x /\ h e. x ) -> ( ( z = ( t \ U. ( x \ { t } ) ) /\ w = ( h \ U. ( x \ { h } ) ) ) -> ( z =/= w -> ( z i^i w ) = (/) ) ) )
31 30 rexlimivv 
 |-  ( E. t e. x E. h e. x ( z = ( t \ U. ( x \ { t } ) ) /\ w = ( h \ U. ( x \ { h } ) ) ) -> ( z =/= w -> ( z i^i w ) = (/) ) )
32 19 31 sylbir 
 |-  ( ( E. t e. x z = ( t \ U. ( x \ { t } ) ) /\ E. h e. x w = ( h \ U. ( x \ { h } ) ) ) -> ( z =/= w -> ( z i^i w ) = (/) ) )
33 5 18 32 syl2anb 
 |-  ( ( z e. A /\ w e. A ) -> ( z =/= w -> ( z i^i w ) = (/) ) )
34 33 rgen2 
 |-  A. z e. A A. w e. A ( z =/= w -> ( z i^i w ) = (/) )