This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐴 ∪ 𝐶 ) ≼* ( 𝐵 ∪ 𝐷 ) )

Proof

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