This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )