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 birani 
 |-  ( ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) -> ( E =/= D /\ F =/= D /\ G =/= D ) )
31 30 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 ) )
32 disjtpsn 
 |-  ( ( E =/= D /\ F =/= D /\ G =/= D ) -> ( { E , F , G } i^i { D } ) = (/) )
33 31 32 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 } ) = (/) )
34 33 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 } ) = (/) )
35 25 34 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 } ) = (/) )
36 24 35 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 } ) = (/) ) )
37 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 } ) = (/) )
38 36 37 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 } ) = (/) )
39 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 } ) ) )
40 4 5 38 39 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 } ) ) )
41 simp3 
 |-  ( ( A =/= B /\ A =/= C /\ A =/= D ) -> A =/= D )
42 41 adantr 
 |-  ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) -> A =/= D )
43 simplr 
 |-  ( ( ( B =/= C /\ B =/= D ) /\ ( B =/= E /\ B =/= F /\ B =/= G ) ) -> B =/= D )
44 simpl 
 |-  ( ( C =/= D /\ ( C =/= E /\ C =/= F /\ C =/= G ) ) -> C =/= D )
45 42 43 44 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 ) )
46 45 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 ) )
47 disjtpsn 
 |-  ( ( A =/= D /\ B =/= D /\ C =/= D ) -> ( { A , B , C } i^i { D } ) = (/) )
48 46 47 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 } ) = (/) )
49 48 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 } ) = (/) )
50 hashun 
 |-  ( ( { A , B , C } e. Fin /\ { D } e. Fin /\ ( { A , B , C } i^i { D } ) = (/) ) -> ( # ` ( { A , B , C } u. { D } ) ) = ( ( # ` { A , B , C } ) + ( # ` { D } ) ) )
51 1 2 49 50 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 } ) ) )
52 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 )
53 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 )
54 simp2 
 |-  ( ( A =/= B /\ A =/= C /\ A =/= D ) -> A =/= C )
55 54 necomd 
 |-  ( ( A =/= B /\ A =/= C /\ A =/= D ) -> C =/= A )
56 55 adantr 
 |-  ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( A =/= E /\ A =/= F /\ A =/= G ) ) -> C =/= A )
57 56 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 )
58 52 53 57 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 ) )
59 58 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 ) )
60 59 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 ) )
61 hashtpg 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( A =/= B /\ B =/= C /\ C =/= A ) <-> ( # ` { A , B , C } ) = 3 ) )
62 61 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 ) )
63 62 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 ) )
64 60 63 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 )
65 hashsng 
 |-  ( D e. V -> ( # ` { D } ) = 1 )
66 65 3ad2ant2 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ D e. V /\ ( E e. V /\ F e. V /\ G e. V ) ) -> ( # ` { D } ) = 1 )
67 66 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 )
68 64 67 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 ) )
69 51 68 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 ) )
70 simp1 
 |-  ( ( E =/= F /\ E =/= G /\ F =/= G ) -> E =/= F )
71 simp3 
 |-  ( ( E =/= F /\ E =/= G /\ F =/= G ) -> F =/= G )
72 simp2 
 |-  ( ( E =/= F /\ E =/= G /\ F =/= G ) -> E =/= G )
73 72 necomd 
 |-  ( ( E =/= F /\ E =/= G /\ F =/= G ) -> G =/= E )
74 70 71 73 3jca 
 |-  ( ( E =/= F /\ E =/= G /\ F =/= G ) -> ( E =/= F /\ F =/= G /\ G =/= E ) )
75 74 adantl 
 |-  ( ( ( D =/= E /\ D =/= F /\ D =/= G ) /\ ( E =/= F /\ E =/= G /\ F =/= G ) ) -> ( E =/= F /\ F =/= G /\ G =/= E ) )
76 75 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 ) )
77 76 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 ) )
78 hashtpg 
 |-  ( ( E e. V /\ F e. V /\ G e. V ) -> ( ( E =/= F /\ F =/= G /\ G =/= E ) <-> ( # ` { E , F , G } ) = 3 ) )
79 78 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 ) )
80 79 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 ) )
81 77 80 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 )
82 69 81 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 ) )
83 3p1e4 
 |-  ( 3 + 1 ) = 4
84 83 oveq1i 
 |-  ( ( 3 + 1 ) + 3 ) = ( 4 + 3 )
85 4p3e7 
 |-  ( 4 + 3 ) = 7
86 84 85 eqtri 
 |-  ( ( 3 + 1 ) + 3 ) = 7
87 82 86 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 )
88 40 87 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 )