Metamath Proof Explorer

Theorem otiunsndisjX

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

Ref Expression
Assertion otiunsndisjX ( 𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑉 ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } )

Proof

Step Hyp Ref Expression
1 orc ⊢ ( 𝑎 = 𝑑 → ( 𝑎 = 𝑑 ∨ ( ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ ) )
2 1 a1d ⊢ ( 𝑎 = 𝑑 → ( ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( 𝑎 = 𝑑 ∨ ( ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ ) ) )
3 eliun ⊢ ( 𝑠 ∈ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ↔ ∃ 𝑐 ∈ 𝑊 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } )
4 simprl ⊢ ( ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → 𝑎 ∈ 𝑉 )
5 4 adantl ⊢ ( ( 𝑐 ∈ 𝑊 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → 𝑎 ∈ 𝑉 )
6 simprl ⊢ ( ( 𝑐 ∈ 𝑊 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → 𝐵 ∈ 𝑋 )
7 simpl ⊢ ( ( 𝑐 ∈ 𝑊 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → 𝑐 ∈ 𝑊 )
8 otthg ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ∧ 𝑐 ∈ 𝑊 ) → ( ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ↔ ( 𝑎 = 𝑑 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑒 ) ) )
9 5 6 7 8 syl3anc ⊢ ( ( 𝑐 ∈ 𝑊 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → ( ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ↔ ( 𝑎 = 𝑑 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑒 ) ) )
10 simp1 ⊢ ( ( 𝑎 = 𝑑 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑒 ) → 𝑎 = 𝑑 )
11 9 10 syl6bi ⊢ ( ( 𝑐 ∈ 𝑊 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → ( ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ → 𝑎 = 𝑑 ) )
12 11 con3d ⊢ ( ( 𝑐 ∈ 𝑊 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → ( ¬ 𝑎 = 𝑑 → ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) )
13 12 ex ⊢ ( 𝑐 ∈ 𝑊 → ( ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( ¬ 𝑎 = 𝑑 → ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) ) )
14 13 com13 ⊢ ( ¬ 𝑎 = 𝑑 → ( ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( 𝑐 ∈ 𝑊 → ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) ) )
15 14 imp31 ⊢ ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) ∧ 𝑐 ∈ 𝑊 ) → ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ )
16 15 adantr ⊢ ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) ∧ 𝑐 ∈ 𝑊 ) ∧ 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ) → ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ )
17 16 adantr ⊢ ( ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) ∧ 𝑐 ∈ 𝑊 ) ∧ 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ) ∧ 𝑒 ∈ 𝑊 ) → ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ )
18 velsn ⊢ ( 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ↔ 𝑠 = ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ )
19 eqeq1 ⊢ ( 𝑠 = ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ → ( 𝑠 = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ↔ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) )
20 19 notbid ⊢ ( 𝑠 = ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ → ( ¬ 𝑠 = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ↔ ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) )
21 18 20 sylbi ⊢ ( 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } → ( ¬ 𝑠 = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ↔ ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) )
22 21 adantl ⊢ ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) ∧ 𝑐 ∈ 𝑊 ) ∧ 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ) → ( ¬ 𝑠 = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ↔ ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) )
23 22 adantr ⊢ ( ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) ∧ 𝑐 ∈ 𝑊 ) ∧ 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ) ∧ 𝑒 ∈ 𝑊 ) → ( ¬ 𝑠 = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ↔ ¬ ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ ) )
24 17 23 mpbird ⊢ ( ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) ∧ 𝑐 ∈ 𝑊 ) ∧ 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ) ∧ 𝑒 ∈ 𝑊 ) → ¬ 𝑠 = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ )
25 velsn ⊢ ( 𝑠 ∈ { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } ↔ 𝑠 = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ )
26 24 25 sylnibr ⊢ ( ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) ∧ 𝑐 ∈ 𝑊 ) ∧ 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ) ∧ 𝑒 ∈ 𝑊 ) → ¬ 𝑠 ∈ { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
27 26 nrexdv ⊢ ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) ∧ 𝑐 ∈ 𝑊 ) ∧ 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ) → ¬ ∃ 𝑒 ∈ 𝑊 𝑠 ∈ { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
28 eliun ⊢ ( 𝑠 ∈ ∪ 𝑒 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } ↔ ∃ 𝑒 ∈ 𝑊 𝑠 ∈ { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
29 27 28 sylnibr ⊢ ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) ∧ 𝑐 ∈ 𝑊 ) ∧ 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ) → ¬ 𝑠 ∈ ∪ 𝑒 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
30 29 rexlimdva2 ⊢ ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → ( ∃ 𝑐 ∈ 𝑊 𝑠 ∈ { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } → ¬ 𝑠 ∈ ∪ 𝑒 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } ) )
31 3 30 syl5bi ⊢ ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → ( 𝑠 ∈ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } → ¬ 𝑠 ∈ ∪ 𝑒 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } ) )
32 31 ralrimiv ⊢ ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → ∀ 𝑠 ∈ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ¬ 𝑠 ∈ ∪ 𝑒 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
33 oteq3 ⊢ ( 𝑐 = 𝑒 → ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ )
34 33 sneqd ⊢ ( 𝑐 = 𝑒 → { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } = { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
35 34 cbviunv ⊢ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } = ∪ 𝑒 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ }
36 35 eleq2i ⊢ ( 𝑠 ∈ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ↔ 𝑠 ∈ ∪ 𝑒 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
37 36 notbii ⊢ ( ¬ 𝑠 ∈ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ↔ ¬ 𝑠 ∈ ∪ 𝑒 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
38 37 ralbii ⊢ ( ∀ 𝑠 ∈ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ¬ 𝑠 ∈ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ↔ ∀ 𝑠 ∈ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ¬ 𝑠 ∈ ∪ 𝑒 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑒 ⟩ } )
39 32 38 sylibr ⊢ ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → ∀ 𝑠 ∈ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ¬ 𝑠 ∈ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } )
40 disj ⊢ ( ( ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ ↔ ∀ 𝑠 ∈ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ¬ 𝑠 ∈ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } )
41 39 40 sylibr ⊢ ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → ( ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ )
42 41 olcd ⊢ ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → ( 𝑎 = 𝑑 ∨ ( ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ ) )
43 42 ex ⊢ ( ¬ 𝑎 = 𝑑 → ( ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( 𝑎 = 𝑑 ∨ ( ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ ) ) )
44 2 43 pm2.61i ⊢ ( ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( 𝑎 = 𝑑 ∨ ( ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ ) )
45 44 ralrimivva ⊢ ( 𝐵 ∈ 𝑋 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ( 𝑎 = 𝑑 ∨ ( ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ ) )
46 oteq1 ⊢ ( 𝑎 = 𝑑 → ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ = ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ )
47 46 sneqd ⊢ ( 𝑎 = 𝑑 → { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } = { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } )
48 47 iuneq2d ⊢ ( 𝑎 = 𝑑 → ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } = ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } )
49 48 disjor ⊢ ( Disj 𝑎 ∈ 𝑉 ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ( 𝑎 = 𝑑 ∨ ( ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } ∩ ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑑 , 𝐵 , 𝑐 ⟩ } ) = ∅ ) )
50 45 49 sylibr ⊢ ( 𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑉 ∪ 𝑐 ∈ 𝑊 { ⟨ 𝑎 , 𝐵 , 𝑐 ⟩ } )