Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( A e. V /\ B e. W ) -> A e. V ) |
2 |
|
0z |
|- 0 e. ZZ |
3 |
1 2
|
jctil |
|- ( ( A e. V /\ B e. W ) -> ( 0 e. ZZ /\ A e. V ) ) |
4 |
3
|
ad2antrr |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( 0 e. ZZ /\ A e. V ) ) |
5 |
|
simpr |
|- ( ( A e. V /\ B e. W ) -> B e. W ) |
6 |
|
1z |
|- 1 e. ZZ |
7 |
5 6
|
jctil |
|- ( ( A e. V /\ B e. W ) -> ( 1 e. ZZ /\ B e. W ) ) |
8 |
7
|
ad2antrr |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( 1 e. ZZ /\ B e. W ) ) |
9 |
4 8
|
jca |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( ( 0 e. ZZ /\ A e. V ) /\ ( 1 e. ZZ /\ B e. W ) ) ) |
10 |
|
id |
|- ( A =/= B -> A =/= B ) |
11 |
10
|
3ad2ant1 |
|- ( ( A =/= B /\ A =/= C /\ A =/= D ) -> A =/= B ) |
12 |
|
0ne1 |
|- 0 =/= 1 |
13 |
11 12
|
jctil |
|- ( ( A =/= B /\ A =/= C /\ A =/= D ) -> ( 0 =/= 1 /\ A =/= B ) ) |
14 |
13
|
adantr |
|- ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( 0 =/= 1 /\ A =/= B ) ) |
15 |
14
|
adantl |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( 0 =/= 1 /\ A =/= B ) ) |
16 |
|
f1oprg |
|- ( ( ( 0 e. ZZ /\ A e. V ) /\ ( 1 e. ZZ /\ B e. W ) ) -> ( ( 0 =/= 1 /\ A =/= B ) -> { <. 0 , A >. , <. 1 , B >. } : { 0 , 1 } -1-1-onto-> { A , B } ) ) |
17 |
9 15 16
|
sylc |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> { <. 0 , A >. , <. 1 , B >. } : { 0 , 1 } -1-1-onto-> { A , B } ) |
18 |
|
simpl |
|- ( ( C e. X /\ D e. Y ) -> C e. X ) |
19 |
|
2nn |
|- 2 e. NN |
20 |
18 19
|
jctil |
|- ( ( C e. X /\ D e. Y ) -> ( 2 e. NN /\ C e. X ) ) |
21 |
20
|
adantl |
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( 2 e. NN /\ C e. X ) ) |
22 |
|
simpr |
|- ( ( C e. X /\ D e. Y ) -> D e. Y ) |
23 |
|
3nn |
|- 3 e. NN |
24 |
22 23
|
jctil |
|- ( ( C e. X /\ D e. Y ) -> ( 3 e. NN /\ D e. Y ) ) |
25 |
24
|
adantl |
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( 3 e. NN /\ D e. Y ) ) |
26 |
21 25
|
jca |
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( ( 2 e. NN /\ C e. X ) /\ ( 3 e. NN /\ D e. Y ) ) ) |
27 |
26
|
adantr |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( ( 2 e. NN /\ C e. X ) /\ ( 3 e. NN /\ D e. Y ) ) ) |
28 |
|
id |
|- ( C =/= D -> C =/= D ) |
29 |
28
|
3ad2ant3 |
|- ( ( B =/= C /\ B =/= D /\ C =/= D ) -> C =/= D ) |
30 |
|
2re |
|- 2 e. RR |
31 |
|
2lt3 |
|- 2 < 3 |
32 |
30 31
|
ltneii |
|- 2 =/= 3 |
33 |
29 32
|
jctil |
|- ( ( B =/= C /\ B =/= D /\ C =/= D ) -> ( 2 =/= 3 /\ C =/= D ) ) |
34 |
33
|
adantl |
|- ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( 2 =/= 3 /\ C =/= D ) ) |
35 |
34
|
adantl |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( 2 =/= 3 /\ C =/= D ) ) |
36 |
|
f1oprg |
|- ( ( ( 2 e. NN /\ C e. X ) /\ ( 3 e. NN /\ D e. Y ) ) -> ( ( 2 =/= 3 /\ C =/= D ) -> { <. 2 , C >. , <. 3 , D >. } : { 2 , 3 } -1-1-onto-> { C , D } ) ) |
37 |
27 35 36
|
sylc |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> { <. 2 , C >. , <. 3 , D >. } : { 2 , 3 } -1-1-onto-> { C , D } ) |
38 |
|
disjsn2 |
|- ( A =/= C -> ( { A } i^i { C } ) = (/) ) |
39 |
38
|
3ad2ant2 |
|- ( ( A =/= B /\ A =/= C /\ A =/= D ) -> ( { A } i^i { C } ) = (/) ) |
40 |
|
disjsn2 |
|- ( B =/= C -> ( { B } i^i { C } ) = (/) ) |
41 |
40
|
3ad2ant1 |
|- ( ( B =/= C /\ B =/= D /\ C =/= D ) -> ( { B } i^i { C } ) = (/) ) |
42 |
39 41
|
anim12i |
|- ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( ( { A } i^i { C } ) = (/) /\ ( { B } i^i { C } ) = (/) ) ) |
43 |
42
|
adantl |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( ( { A } i^i { C } ) = (/) /\ ( { B } i^i { C } ) = (/) ) ) |
44 |
|
df-pr |
|- { A , B } = ( { A } u. { B } ) |
45 |
44
|
ineq1i |
|- ( { A , B } i^i { C } ) = ( ( { A } u. { B } ) i^i { C } ) |
46 |
45
|
eqeq1i |
|- ( ( { A , B } i^i { C } ) = (/) <-> ( ( { A } u. { B } ) i^i { C } ) = (/) ) |
47 |
|
undisj1 |
|- ( ( ( { A } i^i { C } ) = (/) /\ ( { B } i^i { C } ) = (/) ) <-> ( ( { A } u. { B } ) i^i { C } ) = (/) ) |
48 |
46 47
|
bitr4i |
|- ( ( { A , B } i^i { C } ) = (/) <-> ( ( { A } i^i { C } ) = (/) /\ ( { B } i^i { C } ) = (/) ) ) |
49 |
43 48
|
sylibr |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( { A , B } i^i { C } ) = (/) ) |
50 |
|
disjsn2 |
|- ( A =/= D -> ( { A } i^i { D } ) = (/) ) |
51 |
50
|
3ad2ant3 |
|- ( ( A =/= B /\ A =/= C /\ A =/= D ) -> ( { A } i^i { D } ) = (/) ) |
52 |
|
disjsn2 |
|- ( B =/= D -> ( { B } i^i { D } ) = (/) ) |
53 |
52
|
3ad2ant2 |
|- ( ( B =/= C /\ B =/= D /\ C =/= D ) -> ( { B } i^i { D } ) = (/) ) |
54 |
51 53
|
anim12i |
|- ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( ( { A } i^i { D } ) = (/) /\ ( { B } i^i { D } ) = (/) ) ) |
55 |
54
|
adantl |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( ( { A } i^i { D } ) = (/) /\ ( { B } i^i { D } ) = (/) ) ) |
56 |
44
|
ineq1i |
|- ( { A , B } i^i { D } ) = ( ( { A } u. { B } ) i^i { D } ) |
57 |
56
|
eqeq1i |
|- ( ( { A , B } i^i { D } ) = (/) <-> ( ( { A } u. { B } ) i^i { D } ) = (/) ) |
58 |
|
undisj1 |
|- ( ( ( { A } i^i { D } ) = (/) /\ ( { B } i^i { D } ) = (/) ) <-> ( ( { A } u. { B } ) i^i { D } ) = (/) ) |
59 |
57 58
|
bitr4i |
|- ( ( { A , B } i^i { D } ) = (/) <-> ( ( { A } i^i { D } ) = (/) /\ ( { B } i^i { D } ) = (/) ) ) |
60 |
55 59
|
sylibr |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( { A , B } i^i { D } ) = (/) ) |
61 |
49 60
|
jca |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( ( { A , B } i^i { C } ) = (/) /\ ( { A , B } i^i { D } ) = (/) ) ) |
62 |
|
undisj2 |
|- ( ( ( { A , B } i^i { C } ) = (/) /\ ( { A , B } i^i { D } ) = (/) ) <-> ( { A , B } i^i ( { C } u. { D } ) ) = (/) ) |
63 |
|
df-pr |
|- { C , D } = ( { C } u. { D } ) |
64 |
63
|
eqcomi |
|- ( { C } u. { D } ) = { C , D } |
65 |
64
|
ineq2i |
|- ( { A , B } i^i ( { C } u. { D } ) ) = ( { A , B } i^i { C , D } ) |
66 |
65
|
eqeq1i |
|- ( ( { A , B } i^i ( { C } u. { D } ) ) = (/) <-> ( { A , B } i^i { C , D } ) = (/) ) |
67 |
62 66
|
bitri |
|- ( ( ( { A , B } i^i { C } ) = (/) /\ ( { A , B } i^i { D } ) = (/) ) <-> ( { A , B } i^i { C , D } ) = (/) ) |
68 |
61 67
|
sylib |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( { A , B } i^i { C , D } ) = (/) ) |
69 |
|
df-pr |
|- { 0 , 1 } = ( { 0 } u. { 1 } ) |
70 |
69
|
eqcomi |
|- ( { 0 } u. { 1 } ) = { 0 , 1 } |
71 |
70
|
ineq1i |
|- ( ( { 0 } u. { 1 } ) i^i { 2 } ) = ( { 0 , 1 } i^i { 2 } ) |
72 |
|
0ne2 |
|- 0 =/= 2 |
73 |
|
disjsn2 |
|- ( 0 =/= 2 -> ( { 0 } i^i { 2 } ) = (/) ) |
74 |
72 73
|
ax-mp |
|- ( { 0 } i^i { 2 } ) = (/) |
75 |
|
1ne2 |
|- 1 =/= 2 |
76 |
|
disjsn2 |
|- ( 1 =/= 2 -> ( { 1 } i^i { 2 } ) = (/) ) |
77 |
75 76
|
ax-mp |
|- ( { 1 } i^i { 2 } ) = (/) |
78 |
74 77
|
pm3.2i |
|- ( ( { 0 } i^i { 2 } ) = (/) /\ ( { 1 } i^i { 2 } ) = (/) ) |
79 |
|
undisj1 |
|- ( ( ( { 0 } i^i { 2 } ) = (/) /\ ( { 1 } i^i { 2 } ) = (/) ) <-> ( ( { 0 } u. { 1 } ) i^i { 2 } ) = (/) ) |
80 |
78 79
|
mpbi |
|- ( ( { 0 } u. { 1 } ) i^i { 2 } ) = (/) |
81 |
71 80
|
eqtr3i |
|- ( { 0 , 1 } i^i { 2 } ) = (/) |
82 |
70
|
ineq1i |
|- ( ( { 0 } u. { 1 } ) i^i { 3 } ) = ( { 0 , 1 } i^i { 3 } ) |
83 |
|
3ne0 |
|- 3 =/= 0 |
84 |
83
|
necomi |
|- 0 =/= 3 |
85 |
|
disjsn2 |
|- ( 0 =/= 3 -> ( { 0 } i^i { 3 } ) = (/) ) |
86 |
84 85
|
ax-mp |
|- ( { 0 } i^i { 3 } ) = (/) |
87 |
|
1re |
|- 1 e. RR |
88 |
|
1lt3 |
|- 1 < 3 |
89 |
87 88
|
ltneii |
|- 1 =/= 3 |
90 |
|
disjsn2 |
|- ( 1 =/= 3 -> ( { 1 } i^i { 3 } ) = (/) ) |
91 |
89 90
|
ax-mp |
|- ( { 1 } i^i { 3 } ) = (/) |
92 |
86 91
|
pm3.2i |
|- ( ( { 0 } i^i { 3 } ) = (/) /\ ( { 1 } i^i { 3 } ) = (/) ) |
93 |
|
undisj1 |
|- ( ( ( { 0 } i^i { 3 } ) = (/) /\ ( { 1 } i^i { 3 } ) = (/) ) <-> ( ( { 0 } u. { 1 } ) i^i { 3 } ) = (/) ) |
94 |
92 93
|
mpbi |
|- ( ( { 0 } u. { 1 } ) i^i { 3 } ) = (/) |
95 |
82 94
|
eqtr3i |
|- ( { 0 , 1 } i^i { 3 } ) = (/) |
96 |
81 95
|
pm3.2i |
|- ( ( { 0 , 1 } i^i { 2 } ) = (/) /\ ( { 0 , 1 } i^i { 3 } ) = (/) ) |
97 |
|
undisj2 |
|- ( ( ( { 0 , 1 } i^i { 2 } ) = (/) /\ ( { 0 , 1 } i^i { 3 } ) = (/) ) <-> ( { 0 , 1 } i^i ( { 2 } u. { 3 } ) ) = (/) ) |
98 |
|
df-pr |
|- { 2 , 3 } = ( { 2 } u. { 3 } ) |
99 |
98
|
eqcomi |
|- ( { 2 } u. { 3 } ) = { 2 , 3 } |
100 |
99
|
ineq2i |
|- ( { 0 , 1 } i^i ( { 2 } u. { 3 } ) ) = ( { 0 , 1 } i^i { 2 , 3 } ) |
101 |
100
|
eqeq1i |
|- ( ( { 0 , 1 } i^i ( { 2 } u. { 3 } ) ) = (/) <-> ( { 0 , 1 } i^i { 2 , 3 } ) = (/) ) |
102 |
97 101
|
bitri |
|- ( ( ( { 0 , 1 } i^i { 2 } ) = (/) /\ ( { 0 , 1 } i^i { 3 } ) = (/) ) <-> ( { 0 , 1 } i^i { 2 , 3 } ) = (/) ) |
103 |
96 102
|
mpbi |
|- ( { 0 , 1 } i^i { 2 , 3 } ) = (/) |
104 |
68 103
|
jctil |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( ( { 0 , 1 } i^i { 2 , 3 } ) = (/) /\ ( { A , B } i^i { C , D } ) = (/) ) ) |
105 |
|
f1oun |
|- ( ( ( { <. 0 , A >. , <. 1 , B >. } : { 0 , 1 } -1-1-onto-> { A , B } /\ { <. 2 , C >. , <. 3 , D >. } : { 2 , 3 } -1-1-onto-> { C , D } ) /\ ( ( { 0 , 1 } i^i { 2 , 3 } ) = (/) /\ ( { A , B } i^i { C , D } ) = (/) ) ) -> ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) ) |
106 |
17 37 104 105
|
syl21anc |
|- ( ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) /\ ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) ) -> ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) ) |
107 |
106
|
ex |
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) ) ) |