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	biimpi	$⊢ (D \neq E \land D \neq F \land D \neq G) \to (E \neq D \land F \neq D \land G \neq D)$
31	30	adantr	$⊢ ((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	31	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)$
33		disjtpsn	$⊢ (E \neq D \land F \neq D \land G \neq D) \to \{E, F, G\} \cap \{D\} = \emptyset$
34	32 33	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$
35	34	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$
36	25 35	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$
37	24 36	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)$
38		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$
39	37 38	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$
40		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\}\|$
41	4 5 39 40	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\}\|$
42		simp3	$⊢ (A \neq B \land A \neq C \land A \neq D) \to A \neq D$
43	42	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$
44		simplr	$⊢ ((B \neq C \land B \neq D) \land (B \neq E \land B \neq F \land B \neq G)) \to B \neq D$
45		simpl	$⊢ (C \neq D \land (C \neq E \land C \neq F \land C \neq G)) \to C \neq D$
46	43 44 45	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)$
47	46	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)$
48		disjtpsn	$⊢ (A \neq D \land B \neq D \land C \neq D) \to \{A, B, C\} \cap \{D\} = \emptyset$
49	47 48	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$
50	49	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$
51		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\}\|$
52	1 2 50 51	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\}\|$
53		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$
54		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$
55		simp2	$⊢ (A \neq B \land A \neq C \land A \neq D) \to A \neq C$
56	55	necomd	$⊢ (A \neq B \land A \neq C \land A \neq D) \to C \neq A$
57	56	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$
58	57	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$
59	53 54 58	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)$
60	59	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)$
61	60	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)$
62		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)$
63	62	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)$
64	63	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)$
65	61 64	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$
66		hashsng	$⊢ D \in V \to \|\{D\}\| = 1$
67	66	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$
68	67	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$
69	65 68	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$
70	52 69	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$
71		simp1	$⊢ (E \neq F \land E \neq G \land F \neq G) \to E \neq F$
72		simp3	$⊢ (E \neq F \land E \neq G \land F \neq G) \to F \neq G$
73		simp2	$⊢ (E \neq F \land E \neq G \land F \neq G) \to E \neq G$
74	73	necomd	$⊢ (E \neq F \land E \neq G \land F \neq G) \to G \neq E$
75	71 72 74	3jca	$⊢ (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	$⊢ ((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 \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	77	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)$
79		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)$
80	79	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)$
81	80	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)$
82	78 81	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$
83	70 82	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$
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	$⊢ (((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$
89	41 88	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