Metamath Proof Explorer

Theorem 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 syl6bi ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ∧ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) ) → ( ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ → 𝑎 = 𝑑 ) )
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 syl5bi ⊢ ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉 ) ) → ( 𝑠 ∈ ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } → ¬ 𝑠 ∈ ∪ 𝑒 ∈ ( 𝑊 ∖ { 𝑑 } ) { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } ) )
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 𝑎 ∈ 𝑉 ∪ 𝑐 ∈ ( 𝑊 ∖ { 𝑎 } ) { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } )