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