Metamath Proof Explorer

Theorem iundisj2

Description: A disjoint union is disjoint. (Contributed by Mario Carneiro, 4-Jul-2014) (Revised by Mario Carneiro, 11-Dec-2016)

Ref Expression
Hypothesis iundisj.1 
|- ( n = k -> A = B )
Assertion iundisj2 
|- Disj_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B )

Proof

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