Metamath Proof Explorer

Theorem otsndisj

Description: The singletons consisting of ordered triples which have distinct third components are disjoint. (Contributed by Alexander van der Vekens, 10-Mar-2018)

		Ref	Expression
	Assertion	otsndisj	$⊢ (A \in X \land B \in Y) \to \underset{c \in V}{Disj} \{⟨A, B, c⟩\}$

Proof

Step	Hyp	Ref	Expression
1		otthg	$⊢ (A \in X \land B \in Y \land c \in V) \to (⟨A, B, c⟩ = ⟨A, B, d⟩ \leftrightarrow (A = A \land B = B \land c = d))$
2	1	3expa	$⊢ ((A \in X \land B \in Y) \land c \in V) \to (⟨A, B, c⟩ = ⟨A, B, d⟩ \leftrightarrow (A = A \land B = B \land c = d))$
3		simp3	$⊢ (A = A \land B = B \land c = d) \to c = d$
4	2 3	biimtrdi	$⊢ ((A \in X \land B \in Y) \land c \in V) \to (⟨A, B, c⟩ = ⟨A, B, d⟩ \to c = d)$
5	4	con3rr3	$⊢ \neg c = d \to (((A \in X \land B \in Y) \land c \in V) \to \neg ⟨A, B, c⟩ = ⟨A, B, d⟩)$
6	5	imp	$⊢ (\neg c = d \land ((A \in X \land B \in Y) \land c \in V)) \to \neg ⟨A, B, c⟩ = ⟨A, B, d⟩$
7	6	neqned	$⊢ (\neg c = d \land ((A \in X \land B \in Y) \land c \in V)) \to ⟨A, B, c⟩ \neq ⟨A, B, d⟩$
8		disjsn2	$⊢ ⟨A, B, c⟩ \neq ⟨A, B, d⟩ \to \{⟨A, B, c⟩\} \cap \{⟨A, B, d⟩\} = \emptyset$
9	7 8	syl	$⊢ (\neg c = d \land ((A \in X \land B \in Y) \land c \in V)) \to \{⟨A, B, c⟩\} \cap \{⟨A, B, d⟩\} = \emptyset$
10	9	expcom	$⊢ ((A \in X \land B \in Y) \land c \in V) \to (\neg c = d \to \{⟨A, B, c⟩\} \cap \{⟨A, B, d⟩\} = \emptyset)$
11	10	orrd	$⊢ ((A \in X \land B \in Y) \land c \in V) \to (c = d \lor \{⟨A, B, c⟩\} \cap \{⟨A, B, d⟩\} = \emptyset)$
12	11	adantrr	$⊢ ((A \in X \land B \in Y) \land (c \in V \land d \in V)) \to (c = d \lor \{⟨A, B, c⟩\} \cap \{⟨A, B, d⟩\} = \emptyset)$
13	12	ralrimivva	$⊢ (A \in X \land B \in Y) \to \forall c \in V \forall d \in V (c = d \lor \{⟨A, B, c⟩\} \cap \{⟨A, B, d⟩\} = \emptyset)$
14		oteq3	$⊢ c = d \to ⟨A, B, c⟩ = ⟨A, B, d⟩$
15	14	sneqd	$⊢ c = d \to \{⟨A, B, c⟩\} = \{⟨A, B, d⟩\}$
16	15	disjor	$⊢ \underset{c \in V}{Disj} \{⟨A, B, c⟩\} \leftrightarrow \forall c \in V \forall d \in V (c = d \lor \{⟨A, B, c⟩\} \cap \{⟨A, B, d⟩\} = \emptyset)$
17	13 16	sylibr	$⊢ (A \in X \land B \in Y) \to \underset{c \in V}{Disj} \{⟨A, B, c⟩\}$