Metamath Proof Explorer


Theorem iundjiunlem

Description: The sets in the sequence F are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses iundjiunlem.z
|- Z = ( ZZ>= ` N )
iundjiunlem.f
|- F = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
iundjiunlem.j
|- ( ph -> J e. Z )
iundjiunlem.k
|- ( ph -> K e. Z )
iundjiunlem.lt
|- ( ph -> J < K )
Assertion iundjiunlem
|- ( ph -> ( ( F ` J ) i^i ( F ` K ) ) = (/) )

Proof

Step Hyp Ref Expression
1 iundjiunlem.z
 |-  Z = ( ZZ>= ` N )
2 iundjiunlem.f
 |-  F = ( n e. Z |-> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) )
3 iundjiunlem.j
 |-  ( ph -> J e. Z )
4 iundjiunlem.k
 |-  ( ph -> K e. Z )
5 iundjiunlem.lt
 |-  ( ph -> J < K )
6 incom
 |-  ( ( F ` J ) i^i ( F ` K ) ) = ( ( F ` K ) i^i ( F ` J ) )
7 simpl
 |-  ( ( ph /\ x e. ( F ` K ) ) -> ph )
8 simpr
 |-  ( ( ph /\ x e. ( F ` K ) ) -> x e. ( F ` K ) )
9 fveq2
 |-  ( n = K -> ( E ` n ) = ( E ` K ) )
10 oveq2
 |-  ( n = K -> ( N ..^ n ) = ( N ..^ K ) )
11 10 iuneq1d
 |-  ( n = K -> U_ i e. ( N ..^ n ) ( E ` i ) = U_ i e. ( N ..^ K ) ( E ` i ) )
12 9 11 difeq12d
 |-  ( n = K -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) = ( ( E ` K ) \ U_ i e. ( N ..^ K ) ( E ` i ) ) )
13 fvex
 |-  ( E ` K ) e. _V
14 13 difexi
 |-  ( ( E ` K ) \ U_ i e. ( N ..^ K ) ( E ` i ) ) e. _V
15 12 2 14 fvmpt
 |-  ( K e. Z -> ( F ` K ) = ( ( E ` K ) \ U_ i e. ( N ..^ K ) ( E ` i ) ) )
16 4 15 syl
 |-  ( ph -> ( F ` K ) = ( ( E ` K ) \ U_ i e. ( N ..^ K ) ( E ` i ) ) )
17 16 adantr
 |-  ( ( ph /\ x e. ( F ` K ) ) -> ( F ` K ) = ( ( E ` K ) \ U_ i e. ( N ..^ K ) ( E ` i ) ) )
18 8 17 eleqtrd
 |-  ( ( ph /\ x e. ( F ` K ) ) -> x e. ( ( E ` K ) \ U_ i e. ( N ..^ K ) ( E ` i ) ) )
19 18 eldifbd
 |-  ( ( ph /\ x e. ( F ` K ) ) -> -. x e. U_ i e. ( N ..^ K ) ( E ` i ) )
20 3 1 eleqtrdi
 |-  ( ph -> J e. ( ZZ>= ` N ) )
21 1 4 eluzelz2d
 |-  ( ph -> K e. ZZ )
22 20 21 5 elfzod
 |-  ( ph -> J e. ( N ..^ K ) )
23 fveq2
 |-  ( i = J -> ( E ` i ) = ( E ` J ) )
24 23 ssiun2s
 |-  ( J e. ( N ..^ K ) -> ( E ` J ) C_ U_ i e. ( N ..^ K ) ( E ` i ) )
25 22 24 syl
 |-  ( ph -> ( E ` J ) C_ U_ i e. ( N ..^ K ) ( E ` i ) )
26 25 ssneld
 |-  ( ph -> ( -. x e. U_ i e. ( N ..^ K ) ( E ` i ) -> -. x e. ( E ` J ) ) )
27 7 19 26 sylc
 |-  ( ( ph /\ x e. ( F ` K ) ) -> -. x e. ( E ` J ) )
28 eldifi
 |-  ( x e. ( ( E ` J ) \ U_ i e. ( N ..^ J ) ( E ` i ) ) -> x e. ( E ` J ) )
29 27 28 nsyl
 |-  ( ( ph /\ x e. ( F ` K ) ) -> -. x e. ( ( E ` J ) \ U_ i e. ( N ..^ J ) ( E ` i ) ) )
30 fveq2
 |-  ( n = J -> ( E ` n ) = ( E ` J ) )
31 oveq2
 |-  ( n = J -> ( N ..^ n ) = ( N ..^ J ) )
32 31 iuneq1d
 |-  ( n = J -> U_ i e. ( N ..^ n ) ( E ` i ) = U_ i e. ( N ..^ J ) ( E ` i ) )
33 30 32 difeq12d
 |-  ( n = J -> ( ( E ` n ) \ U_ i e. ( N ..^ n ) ( E ` i ) ) = ( ( E ` J ) \ U_ i e. ( N ..^ J ) ( E ` i ) ) )
34 fvex
 |-  ( E ` J ) e. _V
35 34 difexi
 |-  ( ( E ` J ) \ U_ i e. ( N ..^ J ) ( E ` i ) ) e. _V
36 33 2 35 fvmpt
 |-  ( J e. Z -> ( F ` J ) = ( ( E ` J ) \ U_ i e. ( N ..^ J ) ( E ` i ) ) )
37 3 36 syl
 |-  ( ph -> ( F ` J ) = ( ( E ` J ) \ U_ i e. ( N ..^ J ) ( E ` i ) ) )
38 37 adantr
 |-  ( ( ph /\ x e. ( F ` K ) ) -> ( F ` J ) = ( ( E ` J ) \ U_ i e. ( N ..^ J ) ( E ` i ) ) )
39 29 38 neleqtrrd
 |-  ( ( ph /\ x e. ( F ` K ) ) -> -. x e. ( F ` J ) )
40 39 ralrimiva
 |-  ( ph -> A. x e. ( F ` K ) -. x e. ( F ` J ) )
41 disj
 |-  ( ( ( F ` K ) i^i ( F ` J ) ) = (/) <-> A. x e. ( F ` K ) -. x e. ( F ` J ) )
42 40 41 sylibr
 |-  ( ph -> ( ( F ` K ) i^i ( F ` J ) ) = (/) )
43 6 42 syl5eq
 |-  ( ph -> ( ( F ` J ) i^i ( F ` K ) ) = (/) )