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 ) |