otiunsndisj

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

		Ref	Expression
	Assertion	otiunsndisj	$⊢ B \in X \to \underset{a \in V}{Disj} ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\}$

Proof

Step	Hyp	Ref	Expression
1		eliun	$⊢ s \in ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\} \leftrightarrow \exists c \in (W ∖ \{a\}) s \in \{⟨a, B, c⟩\}$
2		otthg	$⊢ (a \in V \land B \in X \land c \in (W ∖ \{a\})) \to (⟨a, B, c⟩ = ⟨d, B, e⟩ \leftrightarrow (a = d \land B = B \land c = e))$
3		simp1	$⊢ (a = d \land B = B \land c = e) \to a = d$
4	2 3	syl6bi	$⊢ (a \in V \land B \in X \land c \in (W ∖ \{a\})) \to (⟨a, B, c⟩ = ⟨d, B, e⟩ \to a = d)$
5	4	con3d	$⊢ (a \in V \land B \in X \land c \in (W ∖ \{a\})) \to (\neg a = d \to \neg ⟨a, B, c⟩ = ⟨d, B, e⟩)$
6	5	3exp	$⊢ a \in V \to (B \in X \to (c \in (W ∖ \{a\}) \to (\neg a = d \to \neg ⟨a, B, c⟩ = ⟨d, B, e⟩)))$
7	6	impcom	$⊢ (B \in X \land a \in V) \to (c \in (W ∖ \{a\}) \to (\neg a = d \to \neg ⟨a, B, c⟩ = ⟨d, B, e⟩))$
8	7	com3r	$⊢ \neg a = d \to ((B \in X \land a \in V) \to (c \in (W ∖ \{a\}) \to \neg ⟨a, B, c⟩ = ⟨d, B, e⟩))$
9	8	imp31	$⊢ ((\neg a = d \land (B \in X \land a \in V)) \land c \in (W ∖ \{a\})) \to \neg ⟨a, B, c⟩ = ⟨d, B, e⟩$
10		velsn	$⊢ s \in \{⟨a, B, c⟩\} \leftrightarrow s = ⟨a, B, c⟩$
11		eqeq1	$⊢ s = ⟨a, B, c⟩ \to (s = ⟨d, B, e⟩ \leftrightarrow ⟨a, B, c⟩ = ⟨d, B, e⟩)$
12	11	notbid	$⊢ s = ⟨a, B, c⟩ \to (\neg s = ⟨d, B, e⟩ \leftrightarrow \neg ⟨a, B, c⟩ = ⟨d, B, e⟩)$
13	10 12	sylbi	$⊢ s \in \{⟨a, B, c⟩\} \to (\neg s = ⟨d, B, e⟩ \leftrightarrow \neg ⟨a, B, c⟩ = ⟨d, B, e⟩)$
14	9 13	syl5ibrcom	$⊢ ((\neg a = d \land (B \in X \land a \in V)) \land c \in (W ∖ \{a\})) \to (s \in \{⟨a, B, c⟩\} \to \neg s = ⟨d, B, e⟩)$
15	14	imp	$⊢ (((\neg a = d \land (B \in X \land a \in V)) \land c \in (W ∖ \{a\})) \land s \in \{⟨a, B, c⟩\}) \to \neg s = ⟨d, B, e⟩$
16		velsn	$⊢ s \in \{⟨d, B, e⟩\} \leftrightarrow s = ⟨d, B, e⟩$
17	15 16	sylnibr	$⊢ (((\neg a = d \land (B \in X \land a \in V)) \land c \in (W ∖ \{a\})) \land s \in \{⟨a, B, c⟩\}) \to \neg s \in \{⟨d, B, e⟩\}$
18	17	adantr	$⊢ ((((\neg a = d \land (B \in X \land a \in V)) \land c \in (W ∖ \{a\})) \land s \in \{⟨a, B, c⟩\}) \land e \in (W ∖ \{d\})) \to \neg s \in \{⟨d, B, e⟩\}$
19	18	nrexdv	$⊢ (((\neg a = d \land (B \in X \land a \in V)) \land c \in (W ∖ \{a\})) \land s \in \{⟨a, B, c⟩\}) \to \neg \exists e \in (W ∖ \{d\}) s \in \{⟨d, B, e⟩\}$
20		eliun	$⊢ s \in ⋃_{e \in W ∖ \{d\}} \{⟨d, B, e⟩\} \leftrightarrow \exists e \in (W ∖ \{d\}) s \in \{⟨d, B, e⟩\}$
21	19 20	sylnibr	$⊢ (((\neg a = d \land (B \in X \land a \in V)) \land c \in (W ∖ \{a\})) \land s \in \{⟨a, B, c⟩\}) \to \neg s \in ⋃_{e \in W ∖ \{d\}} \{⟨d, B, e⟩\}$
22	21	rexlimdva2	$⊢ (\neg a = d \land (B \in X \land a \in V)) \to (\exists c \in (W ∖ \{a\}) s \in \{⟨a, B, c⟩\} \to \neg s \in ⋃_{e \in W ∖ \{d\}} \{⟨d, B, e⟩\})$
23	1 22	syl5bi	$⊢ (\neg a = d \land (B \in X \land a \in V)) \to (s \in ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\} \to \neg s \in ⋃_{e \in W ∖ \{d\}} \{⟨d, B, e⟩\})$
24	23	ralrimiv	$⊢ (\neg a = d \land (B \in X \land a \in V)) \to \forall s \in ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\} \neg s \in ⋃_{e \in W ∖ \{d\}} \{⟨d, B, e⟩\}$
25		oteq3	$⊢ c = e \to ⟨d, B, c⟩ = ⟨d, B, e⟩$
26	25	sneqd	$⊢ c = e \to \{⟨d, B, c⟩\} = \{⟨d, B, e⟩\}$
27	26	cbviunv	$⊢ ⋃_{c \in W ∖ \{d\}} \{⟨d, B, c⟩\} = ⋃_{e \in W ∖ \{d\}} \{⟨d, B, e⟩\}$
28	27	eleq2i	$⊢ s \in ⋃_{c \in W ∖ \{d\}} \{⟨d, B, c⟩\} \leftrightarrow s \in ⋃_{e \in W ∖ \{d\}} \{⟨d, B, e⟩\}$
29	28	notbii	$⊢ \neg s \in ⋃_{c \in W ∖ \{d\}} \{⟨d, B, c⟩\} \leftrightarrow \neg s \in ⋃_{e \in W ∖ \{d\}} \{⟨d, B, e⟩\}$
30	29	ralbii	$⊢ \forall s \in ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\} \neg s \in ⋃_{c \in W ∖ \{d\}} \{⟨d, B, c⟩\} \leftrightarrow \forall s \in ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\} \neg s \in ⋃_{e \in W ∖ \{d\}} \{⟨d, B, e⟩\}$
31	24 30	sylibr	$⊢ (\neg a = d \land (B \in X \land a \in V)) \to \forall s \in ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\} \neg s \in ⋃_{c \in W ∖ \{d\}} \{⟨d, B, c⟩\}$
32		disj	$⊢ ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\} \cap ⋃_{c \in W ∖ \{d\}} \{⟨d, B, c⟩\} = \emptyset \leftrightarrow \forall s \in ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\} \neg s \in ⋃_{c \in W ∖ \{d\}} \{⟨d, B, c⟩\}$
33	31 32	sylibr	$⊢ (\neg a = d \land (B \in X \land a \in V)) \to ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\} \cap ⋃_{c \in W ∖ \{d\}} \{⟨d, B, c⟩\} = \emptyset$
34	33	expcom	$⊢ (B \in X \land a \in V) \to (\neg a = d \to ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\} \cap ⋃_{c \in W ∖ \{d\}} \{⟨d, B, c⟩\} = \emptyset)$
35	34	orrd	$⊢ (B \in X \land a \in V) \to (a = d \lor ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\} \cap ⋃_{c \in W ∖ \{d\}} \{⟨d, B, c⟩\} = \emptyset)$
36	35	adantrr	$⊢ (B \in X \land (a \in V \land d \in V)) \to (a = d \lor ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\} \cap ⋃_{c \in W ∖ \{d\}} \{⟨d, B, c⟩\} = \emptyset)$
37	36	ralrimivva	$⊢ B \in X \to \forall a \in V \forall d \in V (a = d \lor ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\} \cap ⋃_{c \in W ∖ \{d\}} \{⟨d, B, c⟩\} = \emptyset)$
38		sneq	$⊢ a = d \to \{a\} = \{d\}$
39	38	difeq2d	$⊢ a = d \to W ∖ \{a\} = W ∖ \{d\}$
40		oteq1	$⊢ a = d \to ⟨a, B, c⟩ = ⟨d, B, c⟩$
41	40	sneqd	$⊢ a = d \to \{⟨a, B, c⟩\} = \{⟨d, B, c⟩\}$
42	39 41	disjiunb	$⊢ \underset{a \in V}{Disj} ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\} \leftrightarrow \forall a \in V \forall d \in V (a = d \lor ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\} \cap ⋃_{c \in W ∖ \{d\}} \{⟨d, B, c⟩\} = \emptyset)$
43	37 42	sylibr	$⊢ B \in X \to \underset{a \in V}{Disj} ⋃_{c \in W ∖ \{a\}} \{⟨a, B, c⟩\}$

Metamath Proof Explorer

Theorem otiunsndisj

Proof