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 birani ⊢ ( ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) → ( 𝐸 ≠ 𝐷 ∧ 𝐹 ≠ 𝐷 ∧ 𝐺 ≠ 𝐷 ) )
31 30 adantl ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) → ( 𝐸 ≠ 𝐷 ∧ 𝐹 ≠ 𝐷 ∧ 𝐺 ≠ 𝐷 ) )
32 disjtpsn ⊢ ( ( 𝐸 ≠ 𝐷 ∧ 𝐹 ≠ 𝐷 ∧ 𝐺 ≠ 𝐷 ) → ( { 𝐸 , 𝐹 , 𝐺 } ∩ { 𝐷 } ) = ∅ )
33 31 32 syl ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) → ( { 𝐸 , 𝐹 , 𝐺 } ∩ { 𝐷 } ) = ∅ )
34 33 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( { 𝐸 , 𝐹 , 𝐺 } ∩ { 𝐷 } ) = ∅ )
35 25 34 eqtrid ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( { 𝐷 } ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ )
36 24 35 jca ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ ∧ ( { 𝐷 } ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ ) )
37 undisj1 ⊢ ( ( ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ ∧ ( { 𝐷 } ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ ) ↔ ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ )
38 36 37 sylib ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ )
39 hashun ⊢ ( ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∈ Fin ∧ { 𝐸 , 𝐹 , 𝐺 } ∈ Fin ∧ ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∩ { 𝐸 , 𝐹 , 𝐺 } ) = ∅ ) → ( ♯ ‘ ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∪ { 𝐸 , 𝐹 , 𝐺 } ) ) = ( ( ♯ ‘ ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) + ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) ) )
40 4 5 38 39 mp3an12i ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( ♯ ‘ ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∪ { 𝐸 , 𝐹 , 𝐺 } ) ) = ( ( ♯ ‘ ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) + ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) ) )
41 simp3 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) → 𝐴 ≠ 𝐷 )
42 41 adantr ⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) → 𝐴 ≠ 𝐷 )
43 simplr ⊢ ( ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) → 𝐵 ≠ 𝐷 )
44 simpl ⊢ ( ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) → 𝐶 ≠ 𝐷 )
45 42 43 44 3anim123i ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) → ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) )
46 45 adantr ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) → ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) )
47 disjtpsn ⊢ ( ( 𝐴 ≠ 𝐷 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷 ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 } ) = ∅ )
48 46 47 syl ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 } ) = ∅ )
49 48 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 } ) = ∅ )
50 hashun ⊢ ( ( { 𝐴 , 𝐵 , 𝐶 } ∈ Fin ∧ { 𝐷 } ∈ Fin ∧ ( { 𝐴 , 𝐵 , 𝐶 } ∩ { 𝐷 } ) = ∅ ) → ( ♯ ‘ ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) = ( ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) + ( ♯ ‘ { 𝐷 } ) ) )
51 1 2 49 50 mp3an12i ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( ♯ ‘ ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) = ( ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) + ( ♯ ‘ { 𝐷 } ) ) )
52 simp1l1 ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) → 𝐴 ≠ 𝐵 )
53 simp2ll ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) → 𝐵 ≠ 𝐶 )
54 simp2 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) → 𝐴 ≠ 𝐶 )
55 54 necomd ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) → 𝐶 ≠ 𝐴 )
56 55 adantr ⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) → 𝐶 ≠ 𝐴 )
57 56 3ad2ant1 ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) → 𝐶 ≠ 𝐴 )
58 52 53 57 3jca ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴 ) )
59 58 adantr ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴 ) )
60 59 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴 ) )
61 hashtpg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴 ) ↔ ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) = 3 ) )
62 61 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴 ) ↔ ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) = 3 ) )
63 62 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴 ) ↔ ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) = 3 ) )
64 60 63 mpbid ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) = 3 )
65 hashsng ⊢ ( 𝐷 ∈ 𝑉 → ( ♯ ‘ { 𝐷 } ) = 1 )
66 65 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → ( ♯ ‘ { 𝐷 } ) = 1 )
67 66 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( ♯ ‘ { 𝐷 } ) = 1 )
68 64 67 oveq12d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( ( ♯ ‘ { 𝐴 , 𝐵 , 𝐶 } ) + ( ♯ ‘ { 𝐷 } ) ) = ( 3 + 1 ) )
69 51 68 eqtrd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( ♯ ‘ ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) = ( 3 + 1 ) )
70 simp1 ⊢ ( ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) → 𝐸 ≠ 𝐹 )
71 simp3 ⊢ ( ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) → 𝐹 ≠ 𝐺 )
72 simp2 ⊢ ( ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) → 𝐸 ≠ 𝐺 )
73 72 necomd ⊢ ( ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) → 𝐺 ≠ 𝐸 )
74 70 71 73 3jca ⊢ ( ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) → ( 𝐸 ≠ 𝐹 ∧ 𝐹 ≠ 𝐺 ∧ 𝐺 ≠ 𝐸 ) )
75 74 adantl ⊢ ( ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) → ( 𝐸 ≠ 𝐹 ∧ 𝐹 ≠ 𝐺 ∧ 𝐺 ≠ 𝐸 ) )
76 75 adantl ⊢ ( ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) → ( 𝐸 ≠ 𝐹 ∧ 𝐹 ≠ 𝐺 ∧ 𝐺 ≠ 𝐸 ) )
77 76 adantl ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( 𝐸 ≠ 𝐹 ∧ 𝐹 ≠ 𝐺 ∧ 𝐺 ≠ 𝐸 ) )
78 hashtpg ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) → ( ( 𝐸 ≠ 𝐹 ∧ 𝐹 ≠ 𝐺 ∧ 𝐺 ≠ 𝐸 ) ↔ ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) = 3 ) )
79 78 3ad2ant3 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) → ( ( 𝐸 ≠ 𝐹 ∧ 𝐹 ≠ 𝐺 ∧ 𝐺 ≠ 𝐸 ) ↔ ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) = 3 ) )
80 79 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( ( 𝐸 ≠ 𝐹 ∧ 𝐹 ≠ 𝐺 ∧ 𝐺 ≠ 𝐸 ) ↔ ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) = 3 ) )
81 77 80 mpbid ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) = 3 )
82 69 81 oveq12d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( ( ♯ ‘ ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) + ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) ) = ( ( 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 ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( ( ♯ ‘ ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) + ( ♯ ‘ { 𝐸 , 𝐹 , 𝐺 } ) ) = 7 )
88 40 87 eqtrd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐷 ∈ 𝑉 ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑉 ) ) ∧ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷 ) ∧ ( 𝐴 ≠ 𝐸 ∧ 𝐴 ≠ 𝐹 ∧ 𝐴 ≠ 𝐺 ) ) ∧ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ ( 𝐵 ≠ 𝐸 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐺 ) ) ∧ ( 𝐶 ≠ 𝐷 ∧ ( 𝐶 ≠ 𝐸 ∧ 𝐶 ≠ 𝐹 ∧ 𝐶 ≠ 𝐺 ) ) ) ∧ ( ( 𝐷 ≠ 𝐸 ∧ 𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐺 ) ∧ ( 𝐸 ≠ 𝐹 ∧ 𝐸 ≠ 𝐺 ∧ 𝐹 ≠ 𝐺 ) ) ) ) → ( ♯ ‘ ( ( { 𝐴 , 𝐵 , 𝐶 } ∪ { 𝐷 } ) ∪ { 𝐸 , 𝐹 , 𝐺 } ) ) = 7 )