Metamath Proof Explorer


Theorem hash7g

Description: The size of an unordered set of seven different elements. (Contributed by AV, 2-Aug-2025)

Ref Expression
Assertion hash7g
|- ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( # ` ( ( { A , B , C } u. { D } ) u. { E , F , G } ) ) = 7 )

Proof

Step Hyp Ref Expression
1 tpfi
 |-  { A , B , C } e. Fin
2 snfi
 |-  { D } e. Fin
3 unfi
 |-  ( ( { A , B , C } e. Fin /\ { D } e. Fin ) -> ( { A , B , C } u. { D } ) e. Fin )
4 1 2 3 mp2an
 |-  ( { A , B , C } u. { D } ) e. Fin
5 tpfi
 |-  { E , F , G } e. Fin
6 simpr1
 |-  ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) -> A =/= E )
7 simpr1
 |-  ( ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) -> B =/= E )
8 simpr1
 |-  ( ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) -> C =/= E )
9 6 7 8 3anim123i
 |-  ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) -> ( A =/= E /\ B =/= E /\ C =/= E ) )
10 9 adantr
 |-  ( ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) -> ( A =/= E /\ B =/= E /\ C =/= E ) )
11 simpr2
 |-  ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) -> A =/= F )
12 simpr2
 |-  ( ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) -> B =/= F )
13 simpr2
 |-  ( ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) -> C =/= F )
14 11 12 13 3anim123i
 |-  ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) -> ( A =/= F /\ B =/= F /\ C =/= F ) )
15 14 adantr
 |-  ( ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) -> ( A =/= F /\ B =/= F /\ C =/= F ) )
16 simp1r3
 |-  ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) -> A =/= G )
17 16 adantr
 |-  ( ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) -> A =/= G )
18 simp2r3
 |-  ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) -> B =/= G )
19 18 adantr
 |-  ( ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) -> B =/= G )
20 simp3r3
 |-  ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) -> C =/= G )
21 20 adantr
 |-  ( ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) -> C =/= G )
22 disjtp2
 |-  ( ( ( A =/= E /\ B =/= E /\ C =/= E ) /\ ( A =/= F /\ B =/= F /\ C =/= F ) /\ ( A =/= G /\ B =/= G /\ C =/= G ) ) -> ( { A , B , C } i^i { E , F , G } ) = (/) )
23 10 15 17 19 21 22 syl113anc
 |-  ( ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) -> ( { A , B , C } i^i { E , F , G } ) = (/) )
24 23 adantl
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( { A , B , C } i^i { E , F , G } ) = (/) )
25 incom
 |-  ( { D } i^i { E , F , G } ) = ( { E , F , G } i^i { D } )
26 necom
 |-  ( D =/= E <-> E =/= D )
27 necom
 |-  ( D =/= F <-> F =/= D )
28 necom
 |-  ( D =/= G <-> G =/= D )
29 26 27 28 3anbi123i
 |-  ( ( D =/= E /\ D =/= F /\ D =/= G ) <-> ( E =/= D /\ F =/= D /\ G =/= D ) )
30 29 biimpi
 |-  ( ( D =/= E /\ D =/= F /\ D =/= G ) -> ( E =/= D /\ F =/= D /\ G =/= D ) )
31 30 adantr
 |-  ( ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) -> ( E =/= D /\ F =/= D /\ G =/= D ) )
32 31 adantl
 |-  ( ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) -> ( E =/= D /\ F =/= D /\ G =/= D ) )
33 disjtpsn
 |-  ( ( E =/= D /\ F =/= D /\ G =/= D ) -> ( { E , F , G } i^i { D } ) = (/) )
34 32 33 syl
 |-  ( ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) -> ( { E , F , G } i^i { D } ) = (/) )
35 34 adantl
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( { E , F , G } i^i { D } ) = (/) )
36 25 35 eqtrid
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( { D } i^i { E , F , G } ) = (/) )
37 24 36 jca
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( ( { A , B , C } i^i { E , F , G } ) = (/) /\ ( { D } i^i { E , F , G } ) = (/) ) )
38 undisj1
 |-  ( ( ( { A , B , C } i^i { E , F , G } ) = (/) /\ ( { D } i^i { E , F , G } ) = (/) ) <-> ( ( { A , B , C } u. { D } ) i^i { E , F , G } ) = (/) )
39 37 38 sylib
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( ( { A , B , C } u. { D } ) i^i { E , F , G } ) = (/) )
40 hashun
 |-  ( ( ( { A , B , C } u. { D } ) e. Fin /\ { E , F , G } e. Fin /\ ( ( { A , B , C } u. { D } ) i^i { E , F , G } ) = (/) ) -> ( # ` ( ( { A , B , C } u. { D } ) u. { E , F , G } ) ) = ( ( # ` ( { A , B , C } u. { D } ) ) + ( # ` { E , F , G } ) ) )
41 4 5 39 40 mp3an12i
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( # ` ( ( { A , B , C } u. { D } ) u. { E , F , G } ) ) = ( ( # ` ( { A , B , C } u. { D } ) ) + ( # ` { E , F , G } ) ) )
42 simp3
 |-  ( ( A =/= B /\ A =/= C /\ A =/= D ) -> A =/= D )
43 42 adantr
 |-  ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) -> A =/= D )
44 simplr
 |-  ( ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) -> B =/= D )
45 simpl
 |-  ( ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) -> C =/= D )
46 43 44 45 3anim123i
 |-  ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) -> ( A =/= D /\ B =/= D /\ C =/= D ) )
47 46 adantr
 |-  ( ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) -> ( A =/= D /\ B =/= D /\ C =/= D ) )
48 disjtpsn
 |-  ( ( A =/= D /\ B =/= D /\ C =/= D ) -> ( { A , B , C } i^i { D } ) = (/) )
49 47 48 syl
 |-  ( ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) -> ( { A , B , C } i^i { D } ) = (/) )
50 49 adantl
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( { A , B , C } i^i { D } ) = (/) )
51 hashun
 |-  ( ( { A , B , C } e. Fin /\ { D } e. Fin /\ ( { A , B , C } i^i { D } ) = (/) ) -> ( # ` ( { A , B , C } u. { D } ) ) = ( ( # ` { A , B , C } ) + ( # ` { D } ) ) )
52 1 2 50 51 mp3an12i
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( # ` ( { A , B , C } u. { D } ) ) = ( ( # ` { A , B , C } ) + ( # ` { D } ) ) )
53 simp1l1
 |-  ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) -> A =/= B )
54 simp2ll
 |-  ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) -> B =/= C )
55 simp2
 |-  ( ( A =/= B /\ A =/= C /\ A =/= D ) -> A =/= C )
56 55 necomd
 |-  ( ( A =/= B /\ A =/= C /\ A =/= D ) -> C =/= A )
57 56 adantr
 |-  ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) -> C =/= A )
58 57 3ad2ant1
 |-  ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) -> C =/= A )
59 53 54 58 3jca
 |-  ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) -> ( A =/= B /\ B =/= C /\ C =/= A ) )
60 59 adantr
 |-  ( ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) -> ( A =/= B /\ B =/= C /\ C =/= A ) )
61 60 adantl
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( A =/= B /\ B =/= C /\ C =/= A ) )
62 hashtpg
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) <-> ( # ` { A , B , C } ) = 3 ) )
63 62 3ad2ant1
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) <-> ( # ` { A , B , C } ) = 3 ) )
64 63 adantr
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) <-> ( # ` { A , B , C } ) = 3 ) )
65 61 64 mpbid
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( # ` { A , B , C } ) = 3 )
66 hashsng
 |-  ( D e. V -> ( # ` { D } ) = 1 )
67 66 3ad2ant2
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> ( # ` { D } ) = 1 )
68 67 adantr
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( # ` { D } ) = 1 )
69 65 68 oveq12d
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( ( # ` { A , B , C } ) + ( # ` { D } ) ) = ( 3 + 1 ) )
70 52 69 eqtrd
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( # ` ( { A , B , C } u. { D } ) ) = ( 3 + 1 ) )
71 simp1
 |-  ( ( E =/= F /\ E =/= G /\ F =/= G ) -> E =/= F )
72 simp3
 |-  ( ( E =/= F /\ E =/= G /\ F =/= G ) -> F =/= G )
73 simp2
 |-  ( ( E =/= F /\ E =/= G /\ F =/= G ) -> E =/= G )
74 73 necomd
 |-  ( ( E =/= F /\ E =/= G /\ F =/= G ) -> G =/= E )
75 71 72 74 3jca
 |-  ( ( E =/= F /\ E =/= G /\ F =/= G ) -> ( E =/= F /\ F =/= G /\ G =/= E ) )
76 75 adantl
 |-  ( ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) -> ( E =/= F /\ F =/= G /\ G =/= E ) )
77 76 adantl
 |-  ( ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) -> ( E =/= F /\ F =/= G /\ G =/= E ) )
78 77 adantl
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( E =/= F /\ F =/= G /\ G =/= E ) )
79 hashtpg
 |-  ( ( E e. V /\ F e. V /\ G e. V ) -> ( ( E =/= F /\ F =/= G /\ G =/= E ) <-> ( # ` { E , F , G } ) = 3 ) )
80 79 3ad2ant3
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> ( ( E =/= F /\ F =/= G /\ G =/= E ) <-> ( # ` { E , F , G } ) = 3 ) )
81 80 adantr
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( ( E =/= F /\ F =/= G /\ G =/= E ) <-> ( # ` { E , F , G } ) = 3 ) )
82 78 81 mpbid
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( # ` { E , F , G } ) = 3 )
83 70 82 oveq12d
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( ( # ` ( { A , B , C } u. { D } ) ) + ( # ` { E , F , G } ) ) = ( ( 3 + 1 ) + 3 ) )
84 3p1e4
 |-  ( 3 + 1 ) = 4
85 84 oveq1i
 |-  ( ( 3 + 1 ) + 3 ) = ( 4 + 3 )
86 4p3e7
 |-  ( 4 + 3 ) = 7
87 85 86 eqtri
 |-  ( ( 3 + 1 ) + 3 ) = 7
88 83 87 eqtrdi
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( ( # ` ( { A , B , C } u. { D } ) ) + ( # ` { E , F , G } ) ) = 7 )
89 41 88 eqtrd
 |-  ( ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) /\ ( ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) /\ ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) /\ ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) ) /\ ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) ) ) -> ( # ` ( ( { A , B , C } u. { D } ) u. { E , F , G } ) ) = 7 )