Metamath Proof Explorer

Theorem unwdomg

Description: Weak dominance of a (disjoint) union. (Contributed by Stefan O'Rear, 13-Feb-2015) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion unwdomg ⊢ A ≼ * B ∧ C ≼ * D ∧ B ∩ D = ∅ → A ∪ C ≼ * B ∪ D

Proof

Step Hyp Ref Expression
1 brwdom3i ⊢ A ≼ * B → ∃ f ∀ a ∈ A ∃ b ∈ B a = f ⁡ b
2 1 3ad2ant1 ⊢ A ≼ * B ∧ C ≼ * D ∧ B ∩ D = ∅ → ∃ f ∀ a ∈ A ∃ b ∈ B a = f ⁡ b
3 brwdom3i ⊢ C ≼ * D → ∃ g ∀ a ∈ C ∃ b ∈ D a = g ⁡ b
4 3 3ad2ant2 ⊢ A ≼ * B ∧ C ≼ * D ∧ B ∩ D = ∅ → ∃ g ∀ a ∈ C ∃ b ∈ D a = g ⁡ b
5 4 adantr ⊢ A ≼ * B ∧ C ≼ * D ∧ B ∩ D = ∅ ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b → ∃ g ∀ a ∈ C ∃ b ∈ D a = g ⁡ b
6 relwdom ⊢ Rel ⁡ ≼ *
7 6 brrelex1i ⊢ A ≼ * B → A ∈ V
8 6 brrelex1i ⊢ C ≼ * D → C ∈ V
9 unexg ⊢ A ∈ V ∧ C ∈ V → A ∪ C ∈ V
10 7 8 9 syl2an ⊢ A ≼ * B ∧ C ≼ * D → A ∪ C ∈ V
11 10 3adant3 ⊢ A ≼ * B ∧ C ≼ * D ∧ B ∩ D = ∅ → A ∪ C ∈ V
12 11 adantr ⊢ A ≼ * B ∧ C ≼ * D ∧ B ∩ D = ∅ ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ a ∈ C ∃ b ∈ D a = g ⁡ b → A ∪ C ∈ V
13 6 brrelex2i ⊢ A ≼ * B → B ∈ V
14 6 brrelex2i ⊢ C ≼ * D → D ∈ V
15 unexg ⊢ B ∈ V ∧ D ∈ V → B ∪ D ∈ V
16 13 14 15 syl2an ⊢ A ≼ * B ∧ C ≼ * D → B ∪ D ∈ V
17 16 3adant3 ⊢ A ≼ * B ∧ C ≼ * D ∧ B ∩ D = ∅ → B ∪ D ∈ V
18 17 adantr ⊢ A ≼ * B ∧ C ≼ * D ∧ B ∩ D = ∅ ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ a ∈ C ∃ b ∈ D a = g ⁡ b → B ∪ D ∈ V
19 elun ⊢ y ∈ A ∪ C ↔ y ∈ A ∨ y ∈ C
20 eqeq1 ⊢ a = y → a = f ⁡ b ↔ y = f ⁡ b
21 20 rexbidv ⊢ a = y → ∃ b ∈ B a = f ⁡ b ↔ ∃ b ∈ B y = f ⁡ b
22 21 rspcva ⊢ y ∈ A ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b → ∃ b ∈ B y = f ⁡ b
23 fveq2 ⊢ b = z → f ⁡ b = f ⁡ z
24 23 eqeq2d ⊢ b = z → y = f ⁡ b ↔ y = f ⁡ z
25 24 cbvrexvw ⊢ ∃ b ∈ B y = f ⁡ b ↔ ∃ z ∈ B y = f ⁡ z
26 ssun1 ⊢ B ⊆ B ∪ D
27 iftrue ⊢ z ∈ B → if z ∈ B f g = f
28 27 fveq1d ⊢ z ∈ B → if z ∈ B f g ⁡ z = f ⁡ z
29 28 eqeq2d ⊢ z ∈ B → y = if z ∈ B f g ⁡ z ↔ y = f ⁡ z
30 29 biimprd ⊢ z ∈ B → y = f ⁡ z → y = if z ∈ B f g ⁡ z
31 30 reximia ⊢ ∃ z ∈ B y = f ⁡ z → ∃ z ∈ B y = if z ∈ B f g ⁡ z
32 ssrexv ⊢ B ⊆ B ∪ D → ∃ z ∈ B y = if z ∈ B f g ⁡ z → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
33 26 31 32 mpsyl ⊢ ∃ z ∈ B y = f ⁡ z → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
34 25 33 sylbi ⊢ ∃ b ∈ B y = f ⁡ b → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
35 22 34 syl ⊢ y ∈ A ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
36 35 ancoms ⊢ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ y ∈ A → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
37 36 adantlr ⊢ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ a ∈ C ∃ b ∈ D a = g ⁡ b ∧ y ∈ A → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
38 37 adantll ⊢ B ∩ D = ∅ ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ a ∈ C ∃ b ∈ D a = g ⁡ b ∧ y ∈ A → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
39 eqeq1 ⊢ a = y → a = g ⁡ b ↔ y = g ⁡ b
40 39 rexbidv ⊢ a = y → ∃ b ∈ D a = g ⁡ b ↔ ∃ b ∈ D y = g ⁡ b
41 fveq2 ⊢ b = z → g ⁡ b = g ⁡ z
42 41 eqeq2d ⊢ b = z → y = g ⁡ b ↔ y = g ⁡ z
43 42 cbvrexvw ⊢ ∃ b ∈ D y = g ⁡ b ↔ ∃ z ∈ D y = g ⁡ z
44 40 43 bitrdi ⊢ a = y → ∃ b ∈ D a = g ⁡ b ↔ ∃ z ∈ D y = g ⁡ z
45 44 rspccva ⊢ ∀ a ∈ C ∃ b ∈ D a = g ⁡ b ∧ y ∈ C → ∃ z ∈ D y = g ⁡ z
46 ssun2 ⊢ D ⊆ B ∪ D
47 minel ⊢ z ∈ D ∧ B ∩ D = ∅ → ¬ z ∈ B
48 47 ancoms ⊢ B ∩ D = ∅ ∧ z ∈ D → ¬ z ∈ B
49 48 iffalsed ⊢ B ∩ D = ∅ ∧ z ∈ D → if z ∈ B f g = g
50 49 fveq1d ⊢ B ∩ D = ∅ ∧ z ∈ D → if z ∈ B f g ⁡ z = g ⁡ z
51 50 eqeq2d ⊢ B ∩ D = ∅ ∧ z ∈ D → y = if z ∈ B f g ⁡ z ↔ y = g ⁡ z
52 51 biimprd ⊢ B ∩ D = ∅ ∧ z ∈ D → y = g ⁡ z → y = if z ∈ B f g ⁡ z
53 52 reximdva ⊢ B ∩ D = ∅ → ∃ z ∈ D y = g ⁡ z → ∃ z ∈ D y = if z ∈ B f g ⁡ z
54 53 imp ⊢ B ∩ D = ∅ ∧ ∃ z ∈ D y = g ⁡ z → ∃ z ∈ D y = if z ∈ B f g ⁡ z
55 ssrexv ⊢ D ⊆ B ∪ D → ∃ z ∈ D y = if z ∈ B f g ⁡ z → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
56 46 54 55 mpsyl ⊢ B ∩ D = ∅ ∧ ∃ z ∈ D y = g ⁡ z → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
57 45 56 sylan2 ⊢ B ∩ D = ∅ ∧ ∀ a ∈ C ∃ b ∈ D a = g ⁡ b ∧ y ∈ C → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
58 57 anassrs ⊢ B ∩ D = ∅ ∧ ∀ a ∈ C ∃ b ∈ D a = g ⁡ b ∧ y ∈ C → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
59 58 adantlrl ⊢ B ∩ D = ∅ ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ a ∈ C ∃ b ∈ D a = g ⁡ b ∧ y ∈ C → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
60 38 59 jaodan ⊢ B ∩ D = ∅ ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ a ∈ C ∃ b ∈ D a = g ⁡ b ∧ y ∈ A ∨ y ∈ C → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
61 19 60 sylan2b ⊢ B ∩ D = ∅ ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ a ∈ C ∃ b ∈ D a = g ⁡ b ∧ y ∈ A ∪ C → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
62 61 expl ⊢ B ∩ D = ∅ → ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ a ∈ C ∃ b ∈ D a = g ⁡ b ∧ y ∈ A ∪ C → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
63 62 3ad2ant3 ⊢ A ≼ * B ∧ C ≼ * D ∧ B ∩ D = ∅ → ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ a ∈ C ∃ b ∈ D a = g ⁡ b ∧ y ∈ A ∪ C → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
64 63 impl ⊢ A ≼ * B ∧ C ≼ * D ∧ B ∩ D = ∅ ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ a ∈ C ∃ b ∈ D a = g ⁡ b ∧ y ∈ A ∪ C → ∃ z ∈ B ∪ D y = if z ∈ B f g ⁡ z
65 12 18 64 wdom2d ⊢ A ≼ * B ∧ C ≼ * D ∧ B ∩ D = ∅ ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ a ∈ C ∃ b ∈ D a = g ⁡ b → A ∪ C ≼ * B ∪ D
66 65 expr ⊢ A ≼ * B ∧ C ≼ * D ∧ B ∩ D = ∅ ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b → ∀ a ∈ C ∃ b ∈ D a = g ⁡ b → A ∪ C ≼ * B ∪ D
67 66 exlimdv ⊢ A ≼ * B ∧ C ≼ * D ∧ B ∩ D = ∅ ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b → ∃ g ∀ a ∈ C ∃ b ∈ D a = g ⁡ b → A ∪ C ≼ * B ∪ D
68 5 67 mpd ⊢ A ≼ * B ∧ C ≼ * D ∧ B ∩ D = ∅ ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b → A ∪ C ≼ * B ∪ D
69 2 68 exlimddv ⊢ A ≼ * B ∧ C ≼ * D ∧ B ∩ D = ∅ → A ∪ C ≼ * B ∪ D