Step |
Hyp |
Ref |
Expression |
1 |
|
hashdmpropge2.a |
|- ( ph -> A e. V ) |
2 |
|
hashdmpropge2.b |
|- ( ph -> B e. W ) |
3 |
|
hashdmpropge2.c |
|- ( ph -> C e. X ) |
4 |
|
hashdmpropge2.d |
|- ( ph -> D e. Y ) |
5 |
|
hashdmpropge2.f |
|- ( ph -> F e. Z ) |
6 |
|
hashdmpropge2.n |
|- ( ph -> A =/= B ) |
7 |
|
hashdmpropge2.s |
|- ( ph -> { <. A , C >. , <. B , D >. } C_ F ) |
8 |
5
|
dmexd |
|- ( ph -> dom F e. _V ) |
9 |
|
dmpropg |
|- ( ( C e. X /\ D e. Y ) -> dom { <. A , C >. , <. B , D >. } = { A , B } ) |
10 |
3 4 9
|
syl2anc |
|- ( ph -> dom { <. A , C >. , <. B , D >. } = { A , B } ) |
11 |
|
dmss |
|- ( { <. A , C >. , <. B , D >. } C_ F -> dom { <. A , C >. , <. B , D >. } C_ dom F ) |
12 |
7 11
|
syl |
|- ( ph -> dom { <. A , C >. , <. B , D >. } C_ dom F ) |
13 |
10 12
|
eqsstrrd |
|- ( ph -> { A , B } C_ dom F ) |
14 |
|
prssg |
|- ( ( A e. V /\ B e. W ) -> ( ( A e. dom F /\ B e. dom F ) <-> { A , B } C_ dom F ) ) |
15 |
1 2 14
|
syl2anc |
|- ( ph -> ( ( A e. dom F /\ B e. dom F ) <-> { A , B } C_ dom F ) ) |
16 |
|
neeq1 |
|- ( a = A -> ( a =/= b <-> A =/= b ) ) |
17 |
|
neeq2 |
|- ( b = B -> ( A =/= b <-> A =/= B ) ) |
18 |
16 17
|
rspc2ev |
|- ( ( A e. dom F /\ B e. dom F /\ A =/= B ) -> E. a e. dom F E. b e. dom F a =/= b ) |
19 |
18
|
3expa |
|- ( ( ( A e. dom F /\ B e. dom F ) /\ A =/= B ) -> E. a e. dom F E. b e. dom F a =/= b ) |
20 |
19
|
expcom |
|- ( A =/= B -> ( ( A e. dom F /\ B e. dom F ) -> E. a e. dom F E. b e. dom F a =/= b ) ) |
21 |
6 20
|
syl |
|- ( ph -> ( ( A e. dom F /\ B e. dom F ) -> E. a e. dom F E. b e. dom F a =/= b ) ) |
22 |
15 21
|
sylbird |
|- ( ph -> ( { A , B } C_ dom F -> E. a e. dom F E. b e. dom F a =/= b ) ) |
23 |
13 22
|
mpd |
|- ( ph -> E. a e. dom F E. b e. dom F a =/= b ) |
24 |
|
hashge2el2difr |
|- ( ( dom F e. _V /\ E. a e. dom F E. b e. dom F a =/= b ) -> 2 <_ ( # ` dom F ) ) |
25 |
8 23 24
|
syl2anc |
|- ( ph -> 2 <_ ( # ` dom F ) ) |