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 
|- F/_ k A
iundisjf.2 
|- F/_ n B
iundisjf.3 
|- ( n = k -> A = B )
Assertion iundisj2f 
|- Disj_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B )

Proof

Step Hyp Ref Expression
1 iundisjf.1 
 |-  F/_ k A
2 iundisjf.2 
 |-  F/_ n B
3 iundisjf.3 
 |-  ( n = k -> A = B )
4 tru 
 |-  T.
5 eqeq12 
 |-  ( ( a = x /\ b = y ) -> ( a = b <-> x = y ) )
6 csbeq1 
 |-  ( a = x -> [_ a / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) = [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) )
7 csbeq1 
 |-  ( b = y -> [_ b / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) = [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) )
8 6 7 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 ) ) )
9 8 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 ) ) = (/) ) )
10 5 9 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 ) ) = (/) ) ) )
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 \ U_ k e. ( 1 ..^ n ) B ) = [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) )
15 csbeq1 
 |-  ( b = x -> [_ b / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) = [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) )
16 14 15 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 ) ) )
17 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 ) )
18 16 17 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 ) ) )
19 18 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 ) ) = (/) ) )
20 13 19 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 ) ) = (/) ) ) )
21 nnssre 
 |-  NN C_ RR
22 21 a1i 
 |-  ( T. -> NN C_ RR )
23 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 ) ) = (/) ) ) )
24 nesym 
 |-  ( y =/= x <-> -. x = y )
25 nnre 
 |-  ( x e. NN -> x e. RR )
26 nnre 
 |-  ( y e. NN -> y e. RR )
27 id 
 |-  ( x <_ y -> x <_ y )
28 leltne 
 |-  ( ( x e. RR /\ y e. RR /\ x <_ y ) -> ( x < y <-> y =/= x ) )
29 25 26 27 28 syl3an 
 |-  ( ( x e. NN /\ y e. NN /\ x <_ y ) -> ( x < y <-> y =/= x ) )
30 vex 
 |-  x e. _V
31 nfcsb1v 
 |-  F/_ n [_ x / n ]_ A
32 nfcv 
 |-  F/_ n ( 1 ..^ x )
33 32 2 nfiun 
 |-  F/_ n U_ k e. ( 1 ..^ x ) B
34 31 33 nfdif 
 |-  F/_ n ( [_ x / n ]_ A \ U_ k e. ( 1 ..^ x ) B )
35 csbeq1a 
 |-  ( n = x -> A = [_ x / n ]_ A )
36 oveq2 
 |-  ( n = x -> ( 1 ..^ n ) = ( 1 ..^ x ) )
37 36 iuneq1d 
 |-  ( n = x -> U_ k e. ( 1 ..^ n ) B = U_ k e. ( 1 ..^ x ) B )
38 35 37 difeq12d 
 |-  ( n = x -> ( A \ U_ k e. ( 1 ..^ n ) B ) = ( [_ x / n ]_ A \ U_ k e. ( 1 ..^ x ) B ) )
39 30 34 38 csbief 
 |-  [_ x / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) = ( [_ x / n ]_ A \ U_ k e. ( 1 ..^ x ) B )
40 vex 
 |-  y e. _V
41 nfcsb1v 
 |-  F/_ n [_ y / n ]_ A
42 nfcv 
 |-  F/_ n ( 1 ..^ y )
43 42 2 nfiun 
 |-  F/_ n U_ k e. ( 1 ..^ y ) B
44 41 43 nfdif 
 |-  F/_ n ( [_ y / n ]_ A \ U_ k e. ( 1 ..^ y ) B )
45 csbeq1a 
 |-  ( n = y -> A = [_ y / n ]_ A )
46 oveq2 
 |-  ( n = y -> ( 1 ..^ n ) = ( 1 ..^ y ) )
47 46 iuneq1d 
 |-  ( n = y -> U_ k e. ( 1 ..^ n ) B = U_ k e. ( 1 ..^ y ) B )
48 45 47 difeq12d 
 |-  ( n = y -> ( A \ U_ k e. ( 1 ..^ n ) B ) = ( [_ y / n ]_ A \ U_ k e. ( 1 ..^ y ) B ) )
49 40 44 48 csbief 
 |-  [_ y / n ]_ ( A \ U_ k e. ( 1 ..^ n ) B ) = ( [_ y / n ]_ A \ U_ k e. ( 1 ..^ y ) B )
50 39 49 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 ) )
51 simp1 
 |-  ( ( x e. NN /\ y e. NN /\ x < y ) -> x e. NN )
52 nnuz 
 |-  NN = ( ZZ>= ` 1 )
53 51 52 eleqtrdi 
 |-  ( ( x e. NN /\ y e. NN /\ x < y ) -> x e. ( ZZ>= ` 1 ) )
54 simp2 
 |-  ( ( x e. NN /\ y e. NN /\ x < y ) -> y e. NN )
55 54 nnzd 
 |-  ( ( x e. NN /\ y e. NN /\ x < y ) -> y e. ZZ )
56 simp3 
 |-  ( ( x e. NN /\ y e. NN /\ x < y ) -> x < y )
57 elfzo2 
 |-  ( x e. ( 1 ..^ y ) <-> ( x e. ( ZZ>= ` 1 ) /\ y e. ZZ /\ x < y ) )
58 53 55 56 57 syl3anbrc 
 |-  ( ( x e. NN /\ y e. NN /\ x < y ) -> x e. ( 1 ..^ y ) )
59 nfcv 
 |-  F/_ k ( 1 ..^ y )
60 nfcv 
 |-  F/_ k x
61 60 1 nfcsbw 
 |-  F/_ k [_ x / n ]_ A
62 nfcv 
 |-  F/_ 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 e. ( 1 ..^ y ) -> [_ x / n ]_ A C_ U_ k e. ( 1 ..^ y ) B )
67 58 66 syl 
 |-  ( ( x e. NN /\ y e. NN /\ x < y ) -> [_ x / n ]_ A C_ U_ k e. ( 1 ..^ y ) B )
68 67 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 )
69 68 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 ) ) )
70 50 69 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 ) ) )
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. 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 ) ) = (/) )
74 73 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 ) ) = (/) ) )
75 74 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 ) ) = (/) ) )
76 29 75 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 ) ) = (/) ) )
77 24 76 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 ) ) = (/) ) )
78 77 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 ) ) = (/) ) )
79 78 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 ) ) = (/) ) )
80 10 20 22 23 79 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 ) ) = (/) ) )
81 4 80 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 ) ) = (/) ) )
82 81 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 ) ) = (/) )
83 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 ) ) = (/) ) )
84 82 83 mpbir 
 |-  Disj_ n e. NN ( A \ U_ k e. ( 1 ..^ n ) B )