Metamath Proof Explorer

Theorem iundisj2fi

Description: A disjoint union is disjoint, finite version. Cf. iundisj2 . (Contributed by Thierry Arnoux, 16-Feb-2017)

Ref Expression
Hypotheses iundisj2fi.0 
|- F/_ n B
iundisj2fi.1 
|- ( n = k -> A = B )
Assertion iundisj2fi 
|- Disj_ n e. ( 1 ..^ N ) ( A \ U_ k e. ( 1 ..^ n ) B )

Proof

Step Hyp Ref Expression
1 iundisj2fi.0 
 |-  F/_ n B
2 iundisj2fi.1 
 |-  ( n = k -> A = B )
3 tru 
 |-  T.
4 eqeq12 
 |-  ( ( a = x /\ b = y ) -> ( a = b <-> x = y ) )
5 csbeq1 
 |-  ( a = x -> [_ a / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) = [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) )
6 csbeq1 
 |-  ( b = y -> [_ b / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) = [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) )
7 5 6 ineqan12d 
 |-  ( ( a = x /\ b = y ) -> ( [_ a / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ b / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) )
8 7 eqeq1d 
 |-  ( ( a = x /\ b = y ) -> ( ( [_ a / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ b / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) <-> ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) )
9 4 8 orbi12d 
 |-  ( ( a = x /\ b = y ) -> ( ( a = b \/ ( [_ a / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ b / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) <-> ( x = y \/ ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) ) )
10 eqeq12 
 |-  ( ( a = y /\ b = x ) -> ( a = b <-> y = x ) )
11 equcom 
 |-  ( y = x <-> x = y )
12 10 11 bitrdi 
 |-  ( ( a = y /\ b = x ) -> ( a = b <-> x = y ) )
13 csbeq1 
 |-  ( a = y -> [_ a / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) = [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) )
14 csbeq1 
 |-  ( b = x -> [_ b / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) = [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) )
15 13 14 ineqan12d 
 |-  ( ( a = y /\ b = x ) -> ( [_ a / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ b / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = ( [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) )
16 incom 
 |-  ( [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) )
17 15 16 eqtrdi 
 |-  ( ( a = y /\ b = x ) -> ( [_ a / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ b / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) )
18 17 eqeq1d 
 |-  ( ( a = y /\ b = x ) -> ( ( [_ a / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ b / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) <-> ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) )
19 12 18 orbi12d 
 |-  ( ( a = y /\ b = x ) -> ( ( a = b \/ ( [_ a / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ b / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) <-> ( x = y \/ ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) ) )
20 fzossnn 
 |-  ( 1 ..^ N ) C_ NN
21 nnssre 
 |-  NN C_ RR
22 20 21 sstri 
 |-  ( 1 ..^ N ) C_ RR
23 22 a1i 
 |-  ( T. -> ( 1 ..^ N ) C_ RR )
24 biidd 
 |-  ( ( T. /\ ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) ) ) -> ( ( x = y \/ ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) <-> ( x = y \/ ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) ) )
25 nesym 
 |-  ( y =/= x <-> -. x = y )
26 22 sseli 
 |-  ( x e. ( 1 ..^ N ) -> x e. RR )
27 22 sseli 
 |-  ( y e. ( 1 ..^ N ) -> y e. RR )
28 id 
 |-  ( x <_ y -> x <_ y )
29 leltne 
 |-  ( ( x e. RR /\ y e. RR /\ x <_ y ) -> ( x < y <-> y =/= x ) )
30 26 27 28 29 syl3an 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x <_ y ) -> ( x < y <-> y =/= x ) )
31 vex 
 |-  x e. _V
32 nfcsb1v 
 |-  F/_ n [_ x / n ]_ A
33 nfcv 
 |-  F/_ n ( 1 ..^ x )
34 33 1 nfiun 
 |-  F/_ n U_ k e. ( 1 ..^ x ) B
35 32 34 nfdif 
 |-  F/_ n ( [_ x / n ]_ A \ U_ k e. ( 1 ..^ x ) B )
36 csbeq1a 
 |-  ( n = x -> A = [_ x / n ]_ A )
37 oveq2 
 |-  ( n = x -> ( 1 ..^ n ) = ( 1 ..^ x ) )
38 37 iuneq1d 
 |-  ( n = x -> U_ k e. ( 1 ..^ n ) B = U_ k e. ( 1 ..^ x ) B )
39 36 38 difeq12d 
 |-  ( n = x -> ( A \ U_ k e. ( 1 ..^ n ) B ) = ( [_ x / n ]_ A \ U_ k e. ( 1 ..^ x ) B ) )
40 31 35 39 csbief 
 |-  [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) = ( [_ x / n ]_ A \ U_ k e. ( 1 ..^ x ) B )
41 vex 
 |-  y e. _V
42 nfcsb1v 
 |-  F/_ n [_ y / n ]_ A
43 nfcv 
 |-  F/_ n ( 1 ..^ y )
44 43 1 nfiun 
 |-  F/_ n U_ k e. ( 1 ..^ y ) B
45 42 44 nfdif 
 |-  F/_ n ( [_ y / n ]_ A \ U_ k e. ( 1 ..^ y ) B )
46 csbeq1a 
 |-  ( n = y -> A = [_ y / n ]_ A )
47 oveq2 
 |-  ( n = y -> ( 1 ..^ n ) = ( 1 ..^ y ) )
48 47 iuneq1d 
 |-  ( n = y -> U_ k e. ( 1 ..^ n ) B = U_ k e. ( 1 ..^ y ) B )
49 46 48 difeq12d 
 |-  ( n = y -> ( A \ U_ k e. ( 1 ..^ n ) B ) = ( [_ y / n ]_ A \ U_ k e. ( 1 ..^ y ) B ) )
50 41 45 49 csbief 
 |-  [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) = ( [_ y / n ]_ A \ U_ k e. ( 1 ..^ y ) B )
51 40 50 ineq12i 
 |-  ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = ( ( [_ x / n ]_ A \ U_ k e. ( 1 ..^ x ) B ) i^i ( [_ y / n ]_ A \ U_ k e. ( 1 ..^ y ) B ) )
52 simp1 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x < y ) -> x e. ( 1 ..^ N ) )
53 20 52 sselid 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x < y ) -> x e. NN )
54 nnuz 
 |-  NN = ( ZZ>= ` 1 )
55 53 54 eleqtrdi 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x < y ) -> x e. ( ZZ>= ` 1 ) )
56 simp2 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x < y ) -> y e. ( 1 ..^ N ) )
57 20 56 sselid 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x < y ) -> y e. NN )
58 57 nnzd 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x < y ) -> y e. ZZ )
59 simp3 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x < y ) -> x < y )
60 elfzo2 
 |-  ( x e. ( 1 ..^ y ) <-> ( x e. ( ZZ>= ` 1 ) /\ y e. ZZ /\ x < y ) )
61 55 58 59 60 syl3anbrc 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x < y ) -> x e. ( 1 ..^ y ) )
62 nfcv 
 |-  F/_ n k
63 62 1 2 csbhypf 
 |-  ( x = k -> [_ x / n ]_ A = B )
64 63 equcoms 
 |-  ( k = x -> [_ x / n ]_ A = B )
65 64 eqcomd 
 |-  ( k = x -> B = [_ x / n ]_ A )
66 65 ssiun2s 
 |-  ( x e. ( 1 ..^ y ) -> [_ x / n ]_ A C_ U_ k e. ( 1 ..^ y ) B )
67 61 66 syl 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x < y ) -> [_ x / n ]_ A C_ U_ k e. ( 1 ..^ y ) B )
68 67 ssdifssd 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x < y ) -> ( [_ x / n ]_ A \ U_ k e. ( 1 ..^ x ) B ) C_ U_ k e. ( 1 ..^ y ) B )
69 68 ssrind 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x < y ) -> ( ( [_ x / n ]_ A \ U_ k e. ( 1 ..^ x ) B ) i^i ( [_ y / n ]_ A \ U_ k e. ( 1 ..^ y ) B ) ) C_ ( U_ k e. ( 1 ..^ y ) B i^i ( [_ y / n ]_ A \ U_ k e. ( 1 ..^ y ) B ) ) )
70 51 69 eqsstrid 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x < y ) -> ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) C_ ( U_ k e. ( 1 ..^ y ) B i^i ( [_ y / n ]_ A \ U_ k e. ( 1 ..^ y ) B ) ) )
71 disjdif 
 |-  ( U_ k e. ( 1 ..^ y ) B i^i ( [_ y / n ]_ A \ U_ k e. ( 1 ..^ y ) B ) ) = (/)
72 sseq0 
 |-  ( ( ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) C_ ( U_ k e. ( 1 ..^ y ) B i^i ( [_ y / n ]_ A \ U_ k e. ( 1 ..^ y ) B ) ) /\ ( U_ k e. ( 1 ..^ y ) B i^i ( [_ y / n ]_ A \ U_ k e. ( 1 ..^ y ) B ) ) = (/) ) -> ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) )
73 70 71 72 sylancl 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x < y ) -> ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) )
74 73 3expia 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) ) -> ( x < y -> ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) )
75 74 3adant3 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x <_ y ) -> ( x < y -> ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) )
76 30 75 sylbird 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x <_ y ) -> ( y =/= x -> ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) )
77 25 76 syl5bir 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x <_ y ) -> ( -. x = y -> ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) )
78 77 orrd 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x <_ y ) -> ( x = y \/ ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) )
79 78 adantl 
 |-  ( ( T. /\ ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) /\ x <_ y ) ) -> ( x = y \/ ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) )
80 9 19 23 24 79 wlogle 
 |-  ( ( T. /\ ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) ) ) -> ( x = y \/ ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) )
81 3 80 mpan 
 |-  ( ( x e. ( 1 ..^ N ) /\ y e. ( 1 ..^ N ) ) -> ( x = y \/ ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) )
82 81 rgen2 
 |-  A. x e. ( 1 ..^ N ) A. y e. ( 1 ..^ N ) ( x = y \/ ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) )
83 disjors 
 |-  ( Disj_ n e. ( 1 ..^ N ) ( A \ U_ k e. ( 1 ..^ n ) B ) <-> A. x e. ( 1 ..^ N ) A. y e. ( 1 ..^ N ) ( x = y \/ ( [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) i^i [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) ) = (/) ) )
84 82 83 mpbir 
 |-  Disj_ n e. ( 1 ..^ N ) ( A \ U_ k e. ( 1 ..^ n ) B )