Metamath Proof Explorer


Theorem iundisj2f

Description: A disjoint union is disjoint. Cf. iundisj2 . (Contributed by Thierry Arnoux, 30-Dec-2016)

Ref Expression
Hypotheses iundisjf.1 _ k A
iundisjf.2 _ n B
iundisjf.3 n = k A = B
Assertion iundisj2f Disj n A k 1 ..^ n B

Proof

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