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	⊢ ( 𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑉 ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		eliun	⊢ ( 𝑠 ∈ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ↔ ∃ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } )
2		otthg	⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) ) → ( ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ↔ ( 𝑎 = 𝑑 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑒 ) ) )
3		simp1	⊢ ( ( 𝑎 = 𝑑 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑒 ) → 𝑎 = 𝑑 )
4	2 3	biimtrdi	⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) ) → ( ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ → 𝑎 = 𝑑 ) )
5	4	con3d	⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) ) → ( ¬ 𝑎 = 𝑑 → ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) )
6	5	3exp	⊢ ( 𝑎 ∈ 𝑉 → ( 𝐵 ∈ 𝑋 → ( 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) → ( ¬ 𝑎 = 𝑑 → ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) ) ) )
7	6	impcom	⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) → ( 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) → ( ¬ 𝑎 = 𝑑 → ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) ) )
8	7	com3r	⊢ ( ¬ 𝑎 = 𝑑 → ( ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) → ( 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) → ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) ) )
9	8	imp31	⊢ ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) ) ∧ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) ) → ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ )
10		velsn	⊢ ( 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ↔ 𝑠 = ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ )
11		eqeq1	⊢ ( 𝑠 = ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ → ( 𝑠 = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ↔ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) )
12	11	notbid	⊢ ( 𝑠 = ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ → ( ¬ 𝑠 = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ↔ ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) )
13	10 12	sylbi	⊢ ( 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } → ( ¬ 𝑠 = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ↔ ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) )
14	9 13	syl5ibrcom	⊢ ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) ) ∧ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) ) → ( 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } → ¬ 𝑠 = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) )
15	14	imp	⊢ ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) ) ∧ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) ) ∧ 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ) → ¬ 𝑠 = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ )
16		velsn	⊢ ( 𝑠 ∈ { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } ↔ 𝑠 = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ )
17	15 16	sylnibr	⊢ ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) ) ∧ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) ) ∧ 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ) → ¬ 𝑠 ∈ { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
18	17	adantr	⊢ ( ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) ) ∧ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) ) ∧ 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ) ∧ 𝑒 ∈ ( 𝑊 ∖ { 𝑑 } ) ) → ¬ 𝑠 ∈ { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
19	18	nrexdv	⊢ ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) ) ∧ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) ) ∧ 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ) → ¬ ∃ 𝑒 ∈ ( 𝑊 ∖ { 𝑑 } ) 𝑠 ∈ { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
20		eliun	⊢ ( 𝑠 ∈ ∪ 𝑒 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } ↔ ∃ 𝑒 ∈ ( 𝑊 ∖ { 𝑑 } ) 𝑠 ∈ { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
21	19 20	sylnibr	⊢ ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) ) ∧ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) ) ∧ 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ) → ¬ 𝑠 ∈ ∪ 𝑒 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
22	21	rexlimdva2	⊢ ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) ) → ( ∃ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } → ¬ 𝑠 ∈ ∪ 𝑒 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } ) )
23	1 22	biimtrid	⊢ ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) ) → ( 𝑠 ∈ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } → ¬ 𝑠 ∈ ∪ 𝑒 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } ) )
24	23	ralrimiv	⊢ ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) ) → ∀ 𝑠 ∈ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ¬ 𝑠 ∈ ∪ 𝑒 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
25		oteq3	⊢ ( 𝑐 = 𝑒 → ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ )
26	25	sneqd	⊢ ( 𝑐 = 𝑒 → { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } = { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
27	26	cbviunv	⊢ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } = ∪ 𝑒 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ }
28	27	eleq2i	⊢ ( 𝑠 ∈ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ↔ 𝑠 ∈ ∪ 𝑒 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
29	28	notbii	⊢ ( ¬ 𝑠 ∈ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ↔ ¬ 𝑠 ∈ ∪ 𝑒 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
30	29	ralbii	⊢ ( ∀ 𝑠 ∈ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ¬ 𝑠 ∈ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ↔ ∀ 𝑠 ∈ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ¬ 𝑠 ∈ ∪ 𝑒 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
31	24 30	sylibr	⊢ ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) ) → ∀ 𝑠 ∈ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ¬ 𝑠 ∈ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } )
32		disj	⊢ ( ( ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ ↔ ∀ 𝑠 ∈ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ¬ 𝑠 ∈ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } )
33	31 32	sylibr	⊢ ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) ) → ( ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ )
34	33	expcom	⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) → ( ¬ 𝑎 = 𝑑 → ( ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ ) )
35	34	orrd	⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) → ( 𝑎 = 𝑑 ∨ ( ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ ) )
36	35	adantrr	⊢ ( ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( 𝑎 = 𝑑 ∨ ( ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ ) )
37	36	ralrimivva	⊢ ( 𝐵 ∈ 𝑋 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ( 𝑎 = 𝑑 ∨ ( ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ ) )
38		sneq	⊢ ( 𝑎 = 𝑑 → { 𝑎 } = { 𝑑 } )
39	38	difeq2d	⊢ ( 𝑎 = 𝑑 → ( 𝑊 ∖ { 𝑎 } ) = ( 𝑊 ∖ { 𝑑 } ) )
40		oteq1	⊢ ( 𝑎 = 𝑑 → ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ )
41	40	sneqd	⊢ ( 𝑎 = 𝑑 → { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } = { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } )
42	39 41	disjiunb	⊢ ( Disj 𝑎 ∈ 𝑉 ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ( 𝑎 = 𝑑 ∨ ( ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ ) )
43	37 42	sylibr	⊢ ( 𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑉 ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } )

Metamath Proof Explorer

Theorem otiunsndisj

Proof