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 ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( ♯ ‘ ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∪ { 𝐸 , 𝐹 , 𝐺 } ) ) = 7 )

Proof

Step Hyp Ref Expression
1 tpfi { 𝐴 , 𝐵 , 𝐶 } ∈ Fin
2 snfi { 𝐷 } ∈ Fin
3 unfi ( ( { 𝐴 , 𝐵 , 𝐶 } ∈ Fin ∧ { 𝐷 } ∈ Fin ) → ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∈ Fin )
4 1 2 3 mp2an ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∈ Fin
5 tpfi { 𝐸 , 𝐹 , 𝐺 } ∈ Fin
6 simpr1 ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) → 𝐴𝐸 )
7 simpr1 ( ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) → 𝐵𝐸 )
8 simpr1 ( ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) → 𝐶𝐸 )
9 6 7 8 3anim123i ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) → ( 𝐴𝐸𝐵𝐸𝐶𝐸 ) )
10 9 adantr ( ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) → ( 𝐴𝐸𝐵𝐸𝐶𝐸 ) )
11 simpr2 ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) → 𝐴𝐹 )
12 simpr2 ( ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) → 𝐵𝐹 )
13 simpr2 ( ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) → 𝐶𝐹 )
14 11 12 13 3anim123i ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) → ( 𝐴𝐹𝐵𝐹𝐶𝐹 ) )
15 14 adantr ( ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) → ( 𝐴𝐹𝐵𝐹𝐶𝐹 ) )
16 simp1r3 ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) → 𝐴𝐺 )
17 16 adantr ( ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) → 𝐴𝐺 )
18 simp2r3 ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) → 𝐵𝐺 )
19 18 adantr ( ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) → 𝐵𝐺 )
20 simp3r3 ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) → 𝐶𝐺 )
21 20 adantr ( ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) → 𝐶𝐺 )
22 disjtp2 ( ( ( 𝐴𝐸𝐵𝐸𝐶𝐸 ) ∧ ( 𝐴𝐹𝐵𝐹𝐶𝐹 ) ∧ ( 𝐴𝐺𝐵𝐺𝐶𝐺 ) ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ )
23 10 15 17 19 21 22 syl113anc ( ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ )
24 23 adantl ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ )
25 incom ( { 𝐷 } ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ( { 𝐸 , 𝐹 , 𝐺 } ∩ { 𝐷 } )
26 necom ( 𝐷𝐸𝐸𝐷 )
27 necom ( 𝐷𝐹𝐹𝐷 )
28 necom ( 𝐷𝐺𝐺𝐷 )
29 26 27 28 3anbi123i ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ↔ ( 𝐸𝐷𝐹𝐷𝐺𝐷 ) )
30 29 biimpi ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) → ( 𝐸𝐷𝐹𝐷𝐺𝐷 ) )
31 30 adantr ( ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) → ( 𝐸𝐷𝐹𝐷𝐺𝐷 ) )
32 31 adantl ( ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) → ( 𝐸𝐷𝐹𝐷𝐺𝐷 ) )
33 disjtpsn ( ( 𝐸𝐷𝐹𝐷𝐺𝐷 ) → ( { 𝐸 , 𝐹 , 𝐺 } ∩ { 𝐷 } ) = ∅ )
34 32 33 syl ( ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) → ( { 𝐸 , 𝐹 , 𝐺 } ∩ { 𝐷 } ) = ∅ )
35 34 adantl ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( { 𝐸 , 𝐹 , 𝐺 } ∩ { 𝐷 } ) = ∅ )
36 25 35 eqtrid ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( { 𝐷 } ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ )
37 24 36 jca ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ ∧ ( { 𝐷 } ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ ) )
38 undisj1 ( ( ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ ∧ ( { 𝐷 } ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ ) ↔ ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ )
39 37 38 sylib ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ )
40 hashun ( ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∈ Fin ∧ { 𝐸 , 𝐹 , 𝐺 } ∈ Fin ∧ ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ ) → ( ♯ ‘ ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∪ { 𝐸 , 𝐹 , 𝐺 } ) ) = ( ( ♯ ‘ ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) + ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) ) )
41 4 5 39 40 mp3an12i ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( ♯ ‘ ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∪ { 𝐸 , 𝐹 , 𝐺 } ) ) = ( ( ♯ ‘ ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) + ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) ) )
42 simp3 ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) → 𝐴𝐷 )
43 42 adantr ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) → 𝐴𝐷 )
44 simplr ( ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) → 𝐵𝐷 )
45 simpl ( ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) → 𝐶𝐷 )
46 43 44 45 3anim123i ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) → ( 𝐴𝐷𝐵𝐷𝐶𝐷 ) )
47 46 adantr ( ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) → ( 𝐴𝐷𝐵𝐷𝐶𝐷 ) )
48 disjtpsn ( ( 𝐴𝐷𝐵𝐷𝐶𝐷 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 } ) = ∅ )
49 47 48 syl ( ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 } ) = ∅ )
50 49 adantl ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 } ) = ∅ )
51 hashun ( ( { 𝐴 , 𝐵 , 𝐶 } ∈ Fin ∧ { 𝐷 } ∈ Fin ∧ ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 } ) = ∅ ) → ( ♯ ‘ ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) = ( ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) + ( ♯ ‘ { 𝐷 } ) ) )
52 1 2 50 51 mp3an12i ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( ♯ ‘ ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) = ( ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) + ( ♯ ‘ { 𝐷 } ) ) )
53 simp1l1 ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) → 𝐴𝐵 )
54 simp2ll ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) → 𝐵𝐶 )
55 simp2 ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) → 𝐴𝐶 )
56 55 necomd ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) → 𝐶𝐴 )
57 56 adantr ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) → 𝐶𝐴 )
58 57 3ad2ant1 ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) → 𝐶𝐴 )
59 53 54 58 3jca ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) → ( 𝐴𝐵𝐵𝐶𝐶𝐴 ) )
60 59 adantr ( ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) → ( 𝐴𝐵𝐵𝐶𝐶𝐴 ) )
61 60 adantl ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( 𝐴𝐵𝐵𝐶𝐶𝐴 ) )
62 hashtpg ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) → ( ( 𝐴𝐵𝐵𝐶𝐶𝐴 ) ↔ ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) = 3 ) )
63 62 3ad2ant1 ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) → ( ( 𝐴𝐵𝐵𝐶𝐶𝐴 ) ↔ ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) = 3 ) )
64 63 adantr ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( ( 𝐴𝐵𝐵𝐶𝐶𝐴 ) ↔ ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) = 3 ) )
65 61 64 mpbid ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) = 3 )
66 hashsng ( 𝐷𝑉 → ( ♯ ‘ { 𝐷 } ) = 1 )
67 66 3ad2ant2 ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) → ( ♯ ‘ { 𝐷 } ) = 1 )
68 67 adantr ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( ♯ ‘ { 𝐷 } ) = 1 )
69 65 68 oveq12d ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) + ( ♯ ‘ { 𝐷 } ) ) = ( 3 + 1 ) )
70 52 69 eqtrd ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( ♯ ‘ ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) = ( 3 + 1 ) )
71 simp1 ( ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) → 𝐸𝐹 )
72 simp3 ( ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) → 𝐹𝐺 )
73 simp2 ( ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) → 𝐸𝐺 )
74 73 necomd ( ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) → 𝐺𝐸 )
75 71 72 74 3jca ( ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) → ( 𝐸𝐹𝐹𝐺𝐺𝐸 ) )
76 75 adantl ( ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) → ( 𝐸𝐹𝐹𝐺𝐺𝐸 ) )
77 76 adantl ( ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) → ( 𝐸𝐹𝐹𝐺𝐺𝐸 ) )
78 77 adantl ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( 𝐸𝐹𝐹𝐺𝐺𝐸 ) )
79 hashtpg ( ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) → ( ( 𝐸𝐹𝐹𝐺𝐺𝐸 ) ↔ ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) = 3 ) )
80 79 3ad2ant3 ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) → ( ( 𝐸𝐹𝐹𝐺𝐺𝐸 ) ↔ ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) = 3 ) )
81 80 adantr ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( ( 𝐸𝐹𝐹𝐺𝐺𝐸 ) ↔ ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) = 3 ) )
82 78 81 mpbid ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) = 3 )
83 70 82 oveq12d ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( ( ♯ ‘ ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) + ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) ) = ( ( 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 ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( ( ♯ ‘ ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) + ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) ) = 7 )
89 41 88 eqtrd ( ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ 𝐷𝑉 ∧ ( 𝐸𝑉𝐹𝑉𝐺𝑉 ) ) ∧ ( ( ( ( 𝐴𝐵𝐴𝐶𝐴𝐷 ) ∧ ( 𝐴𝐸𝐴𝐹𝐴𝐺 ) ) ∧ ( ( 𝐵𝐶𝐵𝐷 ) ∧ ( 𝐵𝐸𝐵𝐹𝐵𝐺 ) ) ∧ ( 𝐶𝐷 ∧ ( 𝐶𝐸𝐶𝐹𝐶𝐺 ) ) ) ∧ ( ( 𝐷𝐸𝐷𝐹𝐷𝐺 ) ∧ ( 𝐸𝐹𝐸𝐺𝐹𝐺 ) ) ) ) → ( ♯ ‘ ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∪ { 𝐸 , 𝐹 , 𝐺 } ) ) = 7 )