hash7g

Description: The size of an unordered set of seven different elements. (Contributed by AV, 2-Aug-2025)

		Ref	Expression
	Assertion	hash7g	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to \|(\{A, B, C\} \cup \{D\}) \cup \{E, F, G\}\| = 7$

Proof

Step	Hyp	Ref	Expression
1		tpfi	$⊢ \{A, B, C\} \in Fin$
2		snfi	$⊢ \{D\} \in Fin$
3		unfi	$⊢ (\{A, B, C\} \in Fin \land \{D\} \in Fin) \to \{A, B, C\} \cup \{D\} \in Fin$
4	1 2 3	mp2an	$⊢ \{A, B, C\} \cup \{D\} \in Fin$
5		tpfi	$⊢ \{E, F, G\} \in Fin$
6		simpr1	$⊢ ((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \to A \neq E$
7		simpr1	$⊢ ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \to B \neq E$
8		simpr1	$⊢ (C \neq D \land (C \neq E \land C \neq F \land C \neq G)) \to C \neq E$
9	6 7 8	3anim123i	$⊢ (((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \to (A \neq E \land B \neq E \land C \neq E)$
10	9	adantr	$⊢ ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G))) \to (A \neq E \land B \neq E \land C \neq E)$
11		simpr2	$⊢ ((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \to A \neq F$
12		simpr2	$⊢ ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \to B \neq F$
13		simpr2	$⊢ (C \neq D \land (C \neq E \land C \neq F \land C \neq G)) \to C \neq F$
14	11 12 13	3anim123i	$⊢ (((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \to (A \neq F \land B \neq F \land C \neq F)$
15	14	adantr	$⊢ ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G))) \to (A \neq F \land B \neq F \land C \neq F)$
16		simp1r3	$⊢ (((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \to A \neq G$
17	16	adantr	$⊢ ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G))) \to A \neq G$
18		simp2r3	$⊢ (((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \to B \neq G$
19	18	adantr	$⊢ ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G))) \to B \neq G$
20		simp3r3	$⊢ (((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \to C \neq G$
21	20	adantr	$⊢ ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G))) \to C \neq G$
22		disjtp2	$⊢ ((A \neq E \land B \neq E \land C \neq E) \land (A \neq F \land B \neq F \land C \neq F) \land (A \neq G \land B \neq G \land C \neq G)) \to \{A, B, C\} \cap \{E, F, G\} = \emptyset$
23	10 15 17 19 21 22	syl113anc	$⊢ ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G))) \to \{A, B, C\} \cap \{E, F, G\} = \emptyset$
24	23	adantl	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to \{A, B, C\} \cap \{E, F, G\} = \emptyset$
25		incom	$⊢ \{D\} \cap \{E, F, G\} = \{E, F, G\} \cap \{D\}$
26		necom	$⊢ D \neq E \leftrightarrow E \neq D$
27		necom	$⊢ D \neq F \leftrightarrow F \neq D$
28		necom	$⊢ D \neq G \leftrightarrow G \neq D$
29	26 27 28	3anbi123i	$⊢ (D \neq E \land D \neq F \land D \neq G) \leftrightarrow (E \neq D \land F \neq D \land G \neq D)$
30	29	birani	$⊢ ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)) \to (E \neq D \land F \neq D \land G \neq D)$
31	30	adantl	$⊢ ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G))) \to (E \neq D \land F \neq D \land G \neq D)$
32		disjtpsn	$⊢ (E \neq D \land F \neq D \land G \neq D) \to \{E, F, G\} \cap \{D\} = \emptyset$
33	31 32	syl	$⊢ ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G))) \to \{E, F, G\} \cap \{D\} = \emptyset$
34	33	adantl	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to \{E, F, G\} \cap \{D\} = \emptyset$
35	25 34	eqtrid	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to \{D\} \cap \{E, F, G\} = \emptyset$
36	24 35	jca	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to (\{A, B, C\} \cap \{E, F, G\} = \emptyset \land \{D\} \cap \{E, F, G\} = \emptyset)$
37		undisj1	$⊢ (\{A, B, C\} \cap \{E, F, G\} = \emptyset \land \{D\} \cap \{E, F, G\} = \emptyset) \leftrightarrow (\{A, B, C\} \cup \{D\}) \cap \{E, F, G\} = \emptyset$
38	36 37	sylib	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to (\{A, B, C\} \cup \{D\}) \cap \{E, F, G\} = \emptyset$
39		hashun	$⊢ (\{A, B, C\} \cup \{D\} \in Fin \land \{E, F, G\} \in Fin \land (\{A, B, C\} \cup \{D\}) \cap \{E, F, G\} = \emptyset) \to \|(\{A, B, C\} \cup \{D\}) \cup \{E, F, G\}\| = \|\{A, B, C\} \cup \{D\}\| + \|\{E, F, G\}\|$
40	4 5 38 39	mp3an12i	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to \|(\{A, B, C\} \cup \{D\}) \cup \{E, F, G\}\| = \|\{A, B, C\} \cup \{D\}\| + \|\{E, F, G\}\|$
41		simp3	$⊢ (A \neq B \land A \neq C \land A \neq D) \to A \neq D$
42	41	adantr	$⊢ ((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \to A \neq D$
43		simplr	$⊢ ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \to B \neq D$
44		simpl	$⊢ (C \neq D \land (C \neq E \land C \neq F \land C \neq G)) \to C \neq D$
45	42 43 44	3anim123i	$⊢ (((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \to (A \neq D \land B \neq D \land C \neq D)$
46	45	adantr	$⊢ ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G))) \to (A \neq D \land B \neq D \land C \neq D)$
47		disjtpsn	$⊢ (A \neq D \land B \neq D \land C \neq D) \to \{A, B, C\} \cap \{D\} = \emptyset$
48	46 47	syl	$⊢ ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G))) \to \{A, B, C\} \cap \{D\} = \emptyset$
49	48	adantl	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to \{A, B, C\} \cap \{D\} = \emptyset$
50		hashun	$⊢ (\{A, B, C\} \in Fin \land \{D\} \in Fin \land \{A, B, C\} \cap \{D\} = \emptyset) \to \|\{A, B, C\} \cup \{D\}\| = \|\{A, B, C\}\| + \|\{D\}\|$
51	1 2 49 50	mp3an12i	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to \|\{A, B, C\} \cup \{D\}\| = \|\{A, B, C\}\| + \|\{D\}\|$
52		simp1l1	$⊢ (((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \to A \neq B$
53		simp2ll	$⊢ (((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \to B \neq C$
54		simp2	$⊢ (A \neq B \land A \neq C \land A \neq D) \to A \neq C$
55	54	necomd	$⊢ (A \neq B \land A \neq C \land A \neq D) \to C \neq A$
56	55	adantr	$⊢ ((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \to C \neq A$
57	56	3ad2ant1	$⊢ (((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \to C \neq A$
58	52 53 57	3jca	$⊢ (((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \to (A \neq B \land B \neq C \land C \neq A)$
59	58	adantr	$⊢ ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G))) \to (A \neq B \land B \neq C \land C \neq A)$
60	59	adantl	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to (A \neq B \land B \neq C \land C \neq A)$
61		hashtpg	$⊢ (A \in V \land B \in V \land C \in V) \to ((A \neq B \land B \neq C \land C \neq A) \leftrightarrow \|\{A, B, C\}\| = 3)$
62	61	3ad2ant1	$⊢ ((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \to ((A \neq B \land B \neq C \land C \neq A) \leftrightarrow \|\{A, B, C\}\| = 3)$
63	62	adantr	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to ((A \neq B \land B \neq C \land C \neq A) \leftrightarrow \|\{A, B, C\}\| = 3)$
64	60 63	mpbid	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to \|\{A, B, C\}\| = 3$
65		hashsng	$⊢ D \in V \to \|\{D\}\| = 1$
66	65	3ad2ant2	$⊢ ((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \to \|\{D\}\| = 1$
67	66	adantr	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to \|\{D\}\| = 1$
68	64 67	oveq12d	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to \|\{A, B, C\}\| + \|\{D\}\| = 3 + 1$
69	51 68	eqtrd	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to \|\{A, B, C\} \cup \{D\}\| = 3 + 1$
70		simp1	$⊢ (E \neq F \land E \neq G \land F \neq G) \to E \neq F$
71		simp3	$⊢ (E \neq F \land E \neq G \land F \neq G) \to F \neq G$
72		simp2	$⊢ (E \neq F \land E \neq G \land F \neq G) \to E \neq G$
73	72	necomd	$⊢ (E \neq F \land E \neq G \land F \neq G) \to G \neq E$
74	70 71 73	3jca	$⊢ (E \neq F \land E \neq G \land F \neq G) \to (E \neq F \land F \neq G \land G \neq E)$
75	74	adantl	$⊢ ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)) \to (E \neq F \land F \neq G \land G \neq E)$
76	75	adantl	$⊢ ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G))) \to (E \neq F \land F \neq G \land G \neq E)$
77	76	adantl	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to (E \neq F \land F \neq G \land G \neq E)$
78		hashtpg	$⊢ (E \in V \land F \in V \land G \in V) \to ((E \neq F \land F \neq G \land G \neq E) \leftrightarrow \|\{E, F, G\}\| = 3)$
79	78	3ad2ant3	$⊢ ((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \to ((E \neq F \land F \neq G \land G \neq E) \leftrightarrow \|\{E, F, G\}\| = 3)$
80	79	adantr	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to ((E \neq F \land F \neq G \land G \neq E) \leftrightarrow \|\{E, F, G\}\| = 3)$
81	77 80	mpbid	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to \|\{E, F, G\}\| = 3$
82	69 81	oveq12d	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to \|\{A, B, C\} \cup \{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 \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to \|\{A, B, C\} \cup \{D\}\| + \|\{E, F, G\}\| = 7$
88	40 87	eqtrd	$⊢ (((A \in V \land B \in V \land C \in V) \land D \in V \land (E \in V \land F \in V \land G \in V)) \land ((((A \neq B \land A \neq C \land A \neq D) \land (A \neq E \land A \neq F \land A \neq G)) \land ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \land (C \neq D \land (C \neq E \land C \neq F \land C \neq G))) \land ((D \neq E \land D \neq F \land D \neq G) \land (E \neq F \land E \neq G \land F \neq G)))) \to \|(\{A, B, C\} \cup \{D\}) \cup \{E, F, G\}\| = 7$

Metamath Proof Explorer

Theorem hash7g

Proof