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