s3sndisj

Description: The singletons consisting of length 3 strings which have distinct third symbols are disjunct. (Contributed by AV, 17-May-2021)

		Ref	Expression
	Assertion	s3sndisj	$⊢ (A \in X \land B \in Y) \to \underset{c \in Z}{Disj} \{⟨“ A B c ”⟩\}$

Proof

Step	Hyp	Ref	Expression
1		orc	$⊢ c = d \to (c = d \lor \{⟨“ A B c ”⟩\} \cap \{⟨“ A B d ”⟩\} = \emptyset)$
2	1	a1d	$⊢ c = d \to (((A \in X \land B \in Y) \land (c \in Z \land d \in Z)) \to (c = d \lor \{⟨“ A B c ”⟩\} \cap \{⟨“ A B d ”⟩\} = \emptyset))$
3		s3cli	$⊢ ⟨“ A B c ”⟩ \in Word V$
4		elex	$⊢ A \in X \to A \in V$
5		elex	$⊢ B \in Y \to B \in V$
6	4 5	anim12i	$⊢ (A \in X \land B \in Y) \to (A \in V \land B \in V)$
7		elex	$⊢ d \in Z \to d \in V$
8	7	adantl	$⊢ (c \in Z \land d \in Z) \to d \in V$
9	6 8	anim12i	$⊢ ((A \in X \land B \in Y) \land (c \in Z \land d \in Z)) \to ((A \in V \land B \in V) \land d \in V)$
10		df-3an	$⊢ (A \in V \land B \in V \land d \in V) \leftrightarrow ((A \in V \land B \in V) \land d \in V)$
11	9 10	sylibr	$⊢ ((A \in X \land B \in Y) \land (c \in Z \land d \in Z)) \to (A \in V \land B \in V \land d \in V)$
12		eqwrds3	$⊢ (⟨“ A B c ”⟩ \in Word V \land (A \in V \land B \in V \land d \in V)) \to (⟨“ A B c ”⟩ = ⟨“ A B d ”⟩ \leftrightarrow (\|⟨“ A B c ”⟩\| = 3 \land (⟨“ A B c ”⟩ (0) = A \land ⟨“ A B c ”⟩ (1) = B \land ⟨“ A B c ”⟩ (2) = d)))$
13	3 11 12	sylancr	$⊢ ((A \in X \land B \in Y) \land (c \in Z \land d \in Z)) \to (⟨“ A B c ”⟩ = ⟨“ A B d ”⟩ \leftrightarrow (\|⟨“ A B c ”⟩\| = 3 \land (⟨“ A B c ”⟩ (0) = A \land ⟨“ A B c ”⟩ (1) = B \land ⟨“ A B c ”⟩ (2) = d)))$
14		s3fv2	$⊢ c \in V \to ⟨“ A B c ”⟩ (2) = c$
15	14	elv	$⊢ ⟨“ A B c ”⟩ (2) = c$
16		simp3	$⊢ (⟨“ A B c ”⟩ (0) = A \land ⟨“ A B c ”⟩ (1) = B \land ⟨“ A B c ”⟩ (2) = d) \to ⟨“ A B c ”⟩ (2) = d$
17	15 16	syl5eqr	$⊢ (⟨“ A B c ”⟩ (0) = A \land ⟨“ A B c ”⟩ (1) = B \land ⟨“ A B c ”⟩ (2) = d) \to c = d$
18	17	adantl	$⊢ (\|⟨“ A B c ”⟩\| = 3 \land (⟨“ A B c ”⟩ (0) = A \land ⟨“ A B c ”⟩ (1) = B \land ⟨“ A B c ”⟩ (2) = d)) \to c = d$
19	13 18	syl6bi	$⊢ ((A \in X \land B \in Y) \land (c \in Z \land d \in Z)) \to (⟨“ A B c ”⟩ = ⟨“ A B d ”⟩ \to c = d)$
20	19	con3rr3	$⊢ \neg c = d \to (((A \in X \land B \in Y) \land (c \in Z \land d \in Z)) \to \neg ⟨“ A B c ”⟩ = ⟨“ A B d ”⟩)$
21	20	imp	$⊢ (\neg c = d \land ((A \in X \land B \in Y) \land (c \in Z \land d \in Z))) \to \neg ⟨“ A B c ”⟩ = ⟨“ A B d ”⟩$
22	21	neqned	$⊢ (\neg c = d \land ((A \in X \land B \in Y) \land (c \in Z \land d \in Z))) \to ⟨“ A B c ”⟩ \neq ⟨“ A B d ”⟩$
23		disjsn2	$⊢ ⟨“ A B c ”⟩ \neq ⟨“ A B d ”⟩ \to \{⟨“ A B c ”⟩\} \cap \{⟨“ A B d ”⟩\} = \emptyset$
24	22 23	syl	$⊢ (\neg c = d \land ((A \in X \land B \in Y) \land (c \in Z \land d \in Z))) \to \{⟨“ A B c ”⟩\} \cap \{⟨“ A B d ”⟩\} = \emptyset$
25	24	olcd	$⊢ (\neg c = d \land ((A \in X \land B \in Y) \land (c \in Z \land d \in Z))) \to (c = d \lor \{⟨“ A B c ”⟩\} \cap \{⟨“ A B d ”⟩\} = \emptyset)$
26	25	ex	$⊢ \neg c = d \to (((A \in X \land B \in Y) \land (c \in Z \land d \in Z)) \to (c = d \lor \{⟨“ A B c ”⟩\} \cap \{⟨“ A B d ”⟩\} = \emptyset))$
27	2 26	pm2.61i	$⊢ ((A \in X \land B \in Y) \land (c \in Z \land d \in Z)) \to (c = d \lor \{⟨“ A B c ”⟩\} \cap \{⟨“ A B d ”⟩\} = \emptyset)$
28	27	ralrimivva	$⊢ (A \in X \land B \in Y) \to \forall c \in Z \forall d \in Z (c = d \lor \{⟨“ A B c ”⟩\} \cap \{⟨“ A B d ”⟩\} = \emptyset)$
29		eqidd	$⊢ c = d \to A = A$
30		eqidd	$⊢ c = d \to B = B$
31		id	$⊢ c = d \to c = d$
32	29 30 31	s3eqd	$⊢ c = d \to ⟨“ A B c ”⟩ = ⟨“ A B d ”⟩$
33	32	sneqd	$⊢ c = d \to \{⟨“ A B c ”⟩\} = \{⟨“ A B d ”⟩\}$
34	33	disjor	$⊢ \underset{c \in Z}{Disj} \{⟨“ A B c ”⟩\} \leftrightarrow \forall c \in Z \forall d \in Z (c = d \lor \{⟨“ A B c ”⟩\} \cap \{⟨“ A B d ”⟩\} = \emptyset)$
35	28 34	sylibr	$⊢ (A \in X \land B \in Y) \to \underset{c \in Z}{Disj} \{⟨“ A B c ”⟩\}$

Metamath Proof Explorer

Theorem s3sndisj

Proof