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 ⊢ B ∈ X → Disj a ∈ V ⋃ c ∈ W a B c

Proof

Step Hyp Ref Expression
1 orc ⊢ a = d → a = d ∨ ⋃ c ∈ W a B c ∩ ⋃ c ∈ W d B c = ∅
2 1 a1d ⊢ a = d → B ∈ X ∧ a ∈ V ∧ d ∈ V → a = d ∨ ⋃ c ∈ W a B c ∩ ⋃ c ∈ W d B c = ∅
3 eliun ⊢ s ∈ ⋃ c ∈ W a B c ↔ ∃ c ∈ W s ∈ a B c
4 simprl ⊢ B ∈ X ∧ a ∈ V ∧ d ∈ V → a ∈ V
5 4 adantl ⊢ c ∈ W ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V → a ∈ V
6 simprl ⊢ c ∈ W ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V → B ∈ X
7 simpl ⊢ c ∈ W ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V → c ∈ W
8 otthg ⊢ a ∈ V ∧ B ∈ X ∧ c ∈ W → a B c = d B e ↔ a = d ∧ B = B ∧ c = e
9 5 6 7 8 syl3anc ⊢ c ∈ W ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V → a B c = d B e ↔ a = d ∧ B = B ∧ c = e
10 simp1 ⊢ a = d ∧ B = B ∧ c = e → a = d
11 9 10 biimtrdi ⊢ c ∈ W ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V → a B c = d B e → a = d
12 11 con3d ⊢ c ∈ W ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V → ¬ a = d → ¬ a B c = d B e
13 12 ex ⊢ c ∈ W → B ∈ X ∧ a ∈ V ∧ d ∈ V → ¬ a = d → ¬ a B c = d B e
14 13 com13 ⊢ ¬ a = d → B ∈ X ∧ a ∈ V ∧ d ∈ V → c ∈ W → ¬ a B c = d B e
15 14 imp31 ⊢ ¬ a = d ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V ∧ c ∈ W → ¬ a B c = d B e
16 15 adantr ⊢ ¬ a = d ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V ∧ c ∈ W ∧ s ∈ a B c → ¬ a B c = d B e
17 16 adantr ⊢ ¬ a = d ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V ∧ c ∈ W ∧ s ∈ a B c ∧ e ∈ W → ¬ a B c = d B e
18 velsn ⊢ s ∈ a B c ↔ s = a B c
19 eqeq1 ⊢ s = a B c → s = d B e ↔ a B c = d B e
20 19 notbid ⊢ s = a B c → ¬ s = d B e ↔ ¬ a B c = d B e
21 18 20 sylbi ⊢ s ∈ a B c → ¬ s = d B e ↔ ¬ a B c = d B e
22 21 adantl ⊢ ¬ a = d ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V ∧ c ∈ W ∧ s ∈ a B c → ¬ s = d B e ↔ ¬ a B c = d B e
23 22 adantr ⊢ ¬ a = d ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V ∧ c ∈ W ∧ s ∈ a B c ∧ e ∈ W → ¬ s = d B e ↔ ¬ a B c = d B e
24 17 23 mpbird ⊢ ¬ a = d ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V ∧ c ∈ W ∧ s ∈ a B c ∧ e ∈ W → ¬ s = d B e
25 velsn ⊢ s ∈ d B e ↔ s = d B e
26 24 25 sylnibr ⊢ ¬ a = d ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V ∧ c ∈ W ∧ s ∈ a B c ∧ e ∈ W → ¬ s ∈ d B e
27 26 nrexdv ⊢ ¬ a = d ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V ∧ c ∈ W ∧ s ∈ a B c → ¬ ∃ e ∈ W s ∈ d B e
28 eliun ⊢ s ∈ ⋃ e ∈ W d B e ↔ ∃ e ∈ W s ∈ d B e
29 27 28 sylnibr ⊢ ¬ a = d ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V ∧ c ∈ W ∧ s ∈ a B c → ¬ s ∈ ⋃ e ∈ W d B e
30 29 rexlimdva2 ⊢ ¬ a = d ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V → ∃ c ∈ W s ∈ a B c → ¬ s ∈ ⋃ e ∈ W d B e
31 3 30 biimtrid ⊢ ¬ a = d ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V → s ∈ ⋃ c ∈ W a B c → ¬ s ∈ ⋃ e ∈ W d B e
32 31 ralrimiv ⊢ ¬ a = d ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V → ∀ s ∈ ⋃ c ∈ W a B c ¬ s ∈ ⋃ e ∈ W d B e
33 oteq3 ⊢ c = e → d B c = d B e
34 33 sneqd ⊢ c = e → d B c = d B e
35 34 cbviunv ⊢ ⋃ c ∈ W d B c = ⋃ e ∈ W d B e
36 35 eleq2i ⊢ s ∈ ⋃ c ∈ W d B c ↔ s ∈ ⋃ e ∈ W d B e
37 36 notbii ⊢ ¬ s ∈ ⋃ c ∈ W d B c ↔ ¬ s ∈ ⋃ e ∈ W d B e
38 37 ralbii ⊢ ∀ s ∈ ⋃ c ∈ W a B c ¬ s ∈ ⋃ c ∈ W d B c ↔ ∀ s ∈ ⋃ c ∈ W a B c ¬ s ∈ ⋃ e ∈ W d B e
39 32 38 sylibr ⊢ ¬ a = d ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V → ∀ s ∈ ⋃ c ∈ W a B c ¬ s ∈ ⋃ c ∈ W d B c
40 disj ⊢ ⋃ c ∈ W a B c ∩ ⋃ c ∈ W d B c = ∅ ↔ ∀ s ∈ ⋃ c ∈ W a B c ¬ s ∈ ⋃ c ∈ W d B c
41 39 40 sylibr ⊢ ¬ a = d ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V → ⋃ c ∈ W a B c ∩ ⋃ c ∈ W d B c = ∅
42 41 olcd ⊢ ¬ a = d ∧ B ∈ X ∧ a ∈ V ∧ d ∈ V → a = d ∨ ⋃ c ∈ W a B c ∩ ⋃ c ∈ W d B c = ∅
43 42 ex ⊢ ¬ a = d → B ∈ X ∧ a ∈ V ∧ d ∈ V → a = d ∨ ⋃ c ∈ W a B c ∩ ⋃ c ∈ W d B c = ∅
44 2 43 pm2.61i ⊢ B ∈ X ∧ a ∈ V ∧ d ∈ V → a = d ∨ ⋃ c ∈ W a B c ∩ ⋃ c ∈ W d B c = ∅
45 44 ralrimivva ⊢ B ∈ X → ∀ a ∈ V ∀ d ∈ V a = d ∨ ⋃ c ∈ W a B c ∩ ⋃ c ∈ W d B c = ∅
46 oteq1 ⊢ a = d → a B c = d B c
47 46 sneqd ⊢ a = d → a B c = d B c
48 47 iuneq2d ⊢ a = d → ⋃ c ∈ W a B c = ⋃ c ∈ W d B c
49 48 disjor ⊢ Disj a ∈ V ⋃ c ∈ W a B c ↔ ∀ a ∈ V ∀ d ∈ V a = d ∨ ⋃ c ∈ W a B c ∩ ⋃ c ∈ W d B c = ∅
50 45 49 sylibr ⊢ B ∈ X → Disj a ∈ V ⋃ c ∈ W a B c