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 A k 1 ..^ n B

Proof

Step Hyp Ref Expression
1 iundisj.1 n = k A = B
2 tru
3 eqeq12 a = x b = y a = b x = y
4 csbeq1 a = x a / n A k 1 ..^ n B = x / n A k 1 ..^ n B
5 csbeq1 b = y b / n A k 1 ..^ n B = y / n A k 1 ..^ n B
6 4 5 ineqan12d a = x b = y a / n A k 1 ..^ n B b / n A k 1 ..^ n B = x / n A k 1 ..^ n B y / n A k 1 ..^ n B
7 6 eqeq1d a = x b = y a / n A k 1 ..^ n B b / n A k 1 ..^ n B = x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
8 3 7 orbi12d a = x b = y a = b a / n A k 1 ..^ n B b / n A k 1 ..^ n B = x = y x / n A k 1 ..^ n B y / n A k 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 k 1 ..^ n B = y / n A k 1 ..^ n B
13 csbeq1 b = x b / n A k 1 ..^ n B = x / n A k 1 ..^ n B
14 12 13 ineqan12d a = y b = x a / n A k 1 ..^ n B b / n A k 1 ..^ n B = y / n A k 1 ..^ n B x / n A k 1 ..^ n B
15 incom y / n A k 1 ..^ n B x / n A k 1 ..^ n B = x / n A k 1 ..^ n B y / n A k 1 ..^ n B
16 14 15 eqtrdi a = y b = x a / n A k 1 ..^ n B b / n A k 1 ..^ n B = x / n A k 1 ..^ n B y / n A k 1 ..^ n B
17 16 eqeq1d a = y b = x a / n A k 1 ..^ n B b / n A k 1 ..^ n B = x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
18 11 17 orbi12d a = y b = x a = b a / n A k 1 ..^ n B b / n A k 1 ..^ n B = x = y x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
19 nnssre
20 19 a1i
21 biidd x y x = y x / n A k 1 ..^ n B y / n A k 1 ..^ n B = x = y x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
22 nesym y x ¬ x = y
23 nnre x x
24 nnre y y
25 id x y x y
26 leltne x y x y x < y y x
27 23 24 25 26 syl3an x y x y x < y y x
28 vex x V
29 nfcsb1v _ n x / n A
30 nfcv _ n k 1 ..^ x B
31 29 30 nfdif _ n x / n A k 1 ..^ x B
32 csbeq1a n = x A = x / n A
33 oveq2 n = x 1 ..^ n = 1 ..^ x
34 33 iuneq1d n = x k 1 ..^ n B = k 1 ..^ x B
35 32 34 difeq12d n = x A k 1 ..^ n B = x / n A k 1 ..^ x B
36 28 31 35 csbief x / n A k 1 ..^ n B = x / n A k 1 ..^ x B
37 vex y V
38 nfcsb1v _ n y / n A
39 nfcv _ n k 1 ..^ y B
40 38 39 nfdif _ n y / n A k 1 ..^ y B
41 csbeq1a n = y A = y / n A
42 oveq2 n = y 1 ..^ n = 1 ..^ y
43 42 iuneq1d n = y k 1 ..^ n B = k 1 ..^ y B
44 41 43 difeq12d n = y A k 1 ..^ n B = y / n A k 1 ..^ y B
45 37 40 44 csbief y / n A k 1 ..^ n B = y / n A k 1 ..^ y B
46 36 45 ineq12i x / n A k 1 ..^ n B y / n A k 1 ..^ n B = x / n A k 1 ..^ x B y / n A k 1 ..^ y B
47 simp1 x y x < y x
48 nnuz = 1
49 47 48 eleqtrdi x y x < y x 1
50 simp2 x y x < y y
51 50 nnzd x y x < y y
52 simp3 x y x < y x < y
53 elfzo2 x 1 ..^ y x 1 y x < y
54 49 51 52 53 syl3anbrc x y x < y x 1 ..^ y
55 nfcv _ n k
56 nfcv _ 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 1 ..^ y x / n A k 1 ..^ y B
61 54 60 syl x y x < y x / n A k 1 ..^ y B
62 61 ssdifssd x y x < y x / n A k 1 ..^ x B k 1 ..^ y B
63 62 ssrind x y x < y x / n A k 1 ..^ x B y / n A k 1 ..^ y B k 1 ..^ y B y / n A k 1 ..^ y B
64 46 63 eqsstrid x y x < y x / n A k 1 ..^ n B y / n A k 1 ..^ n B k 1 ..^ y B y / n A k 1 ..^ y B
65 disjdif k 1 ..^ y B y / n A k 1 ..^ y B =
66 sseq0 x / n A k 1 ..^ n B y / n A k 1 ..^ n B k 1 ..^ y B y / n A k 1 ..^ y B k 1 ..^ y B y / n A k 1 ..^ y B = x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
67 64 65 66 sylancl x y x < y x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
68 67 3expia x y x < y x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
69 68 3adant3 x y x y x < y x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
70 27 69 sylbird x y x y y x x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
71 22 70 syl5bir x y x y ¬ x = y x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
72 71 orrd x y x y x = y x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
73 72 adantl x y x y x = y x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
74 8 18 20 21 73 wlogle x y x = y x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
75 2 74 mpan x y x = y x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
76 75 rgen2 x y x = y x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
77 disjors Disj n A k 1 ..^ n B x y x = y x / n A k 1 ..^ n B y / n A k 1 ..^ n B =
78 76 77 mpbir Disj n A k 1 ..^ n B