Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( A e. V /\ B e. W ) -> B e. W ) |
2 |
|
elsni |
|- ( B e. { A } -> B = A ) |
3 |
2
|
eqcomd |
|- ( B e. { A } -> A = B ) |
4 |
3
|
necon3ai |
|- ( A =/= B -> -. B e. { A } ) |
5 |
|
snfi |
|- { A } e. Fin |
6 |
|
hashunsng |
|- ( B e. W -> ( ( { A } e. Fin /\ -. B e. { A } ) -> ( # ` ( { A } u. { B } ) ) = ( ( # ` { A } ) + 1 ) ) ) |
7 |
6
|
imp |
|- ( ( B e. W /\ ( { A } e. Fin /\ -. B e. { A } ) ) -> ( # ` ( { A } u. { B } ) ) = ( ( # ` { A } ) + 1 ) ) |
8 |
5 7
|
mpanr1 |
|- ( ( B e. W /\ -. B e. { A } ) -> ( # ` ( { A } u. { B } ) ) = ( ( # ` { A } ) + 1 ) ) |
9 |
1 4 8
|
syl2an |
|- ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> ( # ` ( { A } u. { B } ) ) = ( ( # ` { A } ) + 1 ) ) |
10 |
|
hashsng |
|- ( A e. V -> ( # ` { A } ) = 1 ) |
11 |
10
|
adantr |
|- ( ( A e. V /\ B e. W ) -> ( # ` { A } ) = 1 ) |
12 |
11
|
adantr |
|- ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> ( # ` { A } ) = 1 ) |
13 |
12
|
oveq1d |
|- ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> ( ( # ` { A } ) + 1 ) = ( 1 + 1 ) ) |
14 |
9 13
|
eqtrd |
|- ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> ( # ` ( { A } u. { B } ) ) = ( 1 + 1 ) ) |
15 |
|
df-pr |
|- { A , B } = ( { A } u. { B } ) |
16 |
15
|
fveq2i |
|- ( # ` { A , B } ) = ( # ` ( { A } u. { B } ) ) |
17 |
|
df-2 |
|- 2 = ( 1 + 1 ) |
18 |
14 16 17
|
3eqtr4g |
|- ( ( ( A e. V /\ B e. W ) /\ A =/= B ) -> ( # ` { A , B } ) = 2 ) |
19 |
|
1ne2 |
|- 1 =/= 2 |
20 |
19
|
a1i |
|- ( ( A e. V /\ B e. W ) -> 1 =/= 2 ) |
21 |
11 20
|
eqnetrd |
|- ( ( A e. V /\ B e. W ) -> ( # ` { A } ) =/= 2 ) |
22 |
|
dfsn2 |
|- { A } = { A , A } |
23 |
|
preq2 |
|- ( A = B -> { A , A } = { A , B } ) |
24 |
22 23
|
eqtr2id |
|- ( A = B -> { A , B } = { A } ) |
25 |
24
|
fveq2d |
|- ( A = B -> ( # ` { A , B } ) = ( # ` { A } ) ) |
26 |
25
|
neeq1d |
|- ( A = B -> ( ( # ` { A , B } ) =/= 2 <-> ( # ` { A } ) =/= 2 ) ) |
27 |
21 26
|
syl5ibrcom |
|- ( ( A e. V /\ B e. W ) -> ( A = B -> ( # ` { A , B } ) =/= 2 ) ) |
28 |
27
|
necon2d |
|- ( ( A e. V /\ B e. W ) -> ( ( # ` { A , B } ) = 2 -> A =/= B ) ) |
29 |
28
|
imp |
|- ( ( ( A e. V /\ B e. W ) /\ ( # ` { A , B } ) = 2 ) -> A =/= B ) |
30 |
18 29
|
impbida |
|- ( ( A e. V /\ B e. W ) -> ( A =/= B <-> ( # ` { A , B } ) = 2 ) ) |