Metamath Proof Explorer

Theorem undom

Description: Dominance law for union. Proposition 4.24(a) of Mendelson p. 257. (Contributed by NM, 3-Sep-2004) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion undom ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐴 ∪ 𝐶 ) ≼ ( 𝐵 ∪ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 reldom ⊢ Rel ≼
2 1 brrelex2i ⊢ ( 𝐴 ≼ 𝐵 → 𝐵 ∈ V )
3 domeng ⊢ ( 𝐵 ∈ V → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) )
4 2 3 syl ⊢ ( 𝐴 ≼ 𝐵 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) )
5 4 ibi ⊢ ( 𝐴 ≼ 𝐵 → ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) )
6 1 brrelex1i ⊢ ( 𝐶 ≼ 𝐷 → 𝐶 ∈ V )
7 difss ⊢ ( 𝐶 ∖ 𝐴 ) ⊆ 𝐶
8 ssdomg ⊢ ( 𝐶 ∈ V → ( ( 𝐶 ∖ 𝐴 ) ⊆ 𝐶 → ( 𝐶 ∖ 𝐴 ) ≼ 𝐶 ) )
9 6 7 8 mpisyl ⊢ ( 𝐶 ≼ 𝐷 → ( 𝐶 ∖ 𝐴 ) ≼ 𝐶 )
10 domtr ⊢ ( ( ( 𝐶 ∖ 𝐴 ) ≼ 𝐶 ∧ 𝐶 ≼ 𝐷 ) → ( 𝐶 ∖ 𝐴 ) ≼ 𝐷 )
11 9 10 mpancom ⊢ ( 𝐶 ≼ 𝐷 → ( 𝐶 ∖ 𝐴 ) ≼ 𝐷 )
12 1 brrelex2i ⊢ ( ( 𝐶 ∖ 𝐴 ) ≼ 𝐷 → 𝐷 ∈ V )
13 domeng ⊢ ( 𝐷 ∈ V → ( ( 𝐶 ∖ 𝐴 ) ≼ 𝐷 ↔ ∃ 𝑦 ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) )
14 12 13 syl ⊢ ( ( 𝐶 ∖ 𝐴 ) ≼ 𝐷 → ( ( 𝐶 ∖ 𝐴 ) ≼ 𝐷 ↔ ∃ 𝑦 ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) )
15 14 ibi ⊢ ( ( 𝐶 ∖ 𝐴 ) ≼ 𝐷 → ∃ 𝑦 ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) )
16 11 15 syl ⊢ ( 𝐶 ≼ 𝐷 → ∃ 𝑦 ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) )
17 5 16 anim12i ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) → ( ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ∃ 𝑦 ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) )
18 17 adantr ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ∃ 𝑦 ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) )
19 exdistrv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) ↔ ( ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ∃ 𝑦 ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) )
20 simprll ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ∧ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) ) → 𝐴 ≈ 𝑥 )
21 simprrl ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ∧ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) ) → ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 )
22 disjdif ⊢ ( 𝐴 ∩ ( 𝐶 ∖ 𝐴 ) ) = ∅
23 22 a1i ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ∧ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) ) → ( 𝐴 ∩ ( 𝐶 ∖ 𝐴 ) ) = ∅ )
24 ss2in ⊢ ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐷 ) → ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝐵 ∩ 𝐷 ) )
25 24 ad2ant2l ⊢ ( ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝐵 ∩ 𝐷 ) )
26 25 adantl ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ∧ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝐵 ∩ 𝐷 ) )
27 simplr ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ∧ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) ) → ( 𝐵 ∩ 𝐷 ) = ∅ )
28 sseq0 ⊢ ( ( ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝐵 ∩ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝑥 ∩ 𝑦 ) = ∅ )
29 26 27 28 syl2anc ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ∧ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) ) → ( 𝑥 ∩ 𝑦 ) = ∅ )
30 undif2 ⊢ ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) = ( 𝐴 ∪ 𝐶 )
31 unen ⊢ ( ( ( 𝐴 ≈ 𝑥 ∧ ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ) ∧ ( ( 𝐴 ∩ ( 𝐶 ∖ 𝐴 ) ) = ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) ≈ ( 𝑥 ∪ 𝑦 ) )
32 30 31 eqbrtrrid ⊢ ( ( ( 𝐴 ≈ 𝑥 ∧ ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ) ∧ ( ( 𝐴 ∩ ( 𝐶 ∖ 𝐴 ) ) = ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( 𝐴 ∪ 𝐶 ) ≈ ( 𝑥 ∪ 𝑦 ) )
33 20 21 23 29 32 syl22anc ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ∧ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) ) → ( 𝐴 ∪ 𝐶 ) ≈ ( 𝑥 ∪ 𝑦 ) )
34 2 ad3antrrr ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ∧ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) ) → 𝐵 ∈ V )
35 1 brrelex2i ⊢ ( 𝐶 ≼ 𝐷 → 𝐷 ∈ V )
36 35 ad3antlr ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ∧ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) ) → 𝐷 ∈ V )
37 unexg ⊢ ( ( 𝐵 ∈ V ∧ 𝐷 ∈ V ) → ( 𝐵 ∪ 𝐷 ) ∈ V )
38 34 36 37 syl2anc ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ∧ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) ) → ( 𝐵 ∪ 𝐷 ) ∈ V )
39 unss12 ⊢ ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐷 ) → ( 𝑥 ∪ 𝑦 ) ⊆ ( 𝐵 ∪ 𝐷 ) )
40 39 ad2ant2l ⊢ ( ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) → ( 𝑥 ∪ 𝑦 ) ⊆ ( 𝐵 ∪ 𝐷 ) )
41 40 adantl ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ∧ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) ) → ( 𝑥 ∪ 𝑦 ) ⊆ ( 𝐵 ∪ 𝐷 ) )
42 ssdomg ⊢ ( ( 𝐵 ∪ 𝐷 ) ∈ V → ( ( 𝑥 ∪ 𝑦 ) ⊆ ( 𝐵 ∪ 𝐷 ) → ( 𝑥 ∪ 𝑦 ) ≼ ( 𝐵 ∪ 𝐷 ) ) )
43 38 41 42 sylc ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ∧ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) ) → ( 𝑥 ∪ 𝑦 ) ≼ ( 𝐵 ∪ 𝐷 ) )
44 endomtr ⊢ ( ( ( 𝐴 ∪ 𝐶 ) ≈ ( 𝑥 ∪ 𝑦 ) ∧ ( 𝑥 ∪ 𝑦 ) ≼ ( 𝐵 ∪ 𝐷 ) ) → ( 𝐴 ∪ 𝐶 ) ≼ ( 𝐵 ∪ 𝐷 ) )
45 33 43 44 syl2anc ⊢ ( ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ∧ ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) ) → ( 𝐴 ∪ 𝐶 ) ≼ ( 𝐵 ∪ 𝐷 ) )
46 45 ex ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) → ( 𝐴 ∪ 𝐶 ) ≼ ( 𝐵 ∪ 𝐷 ) ) )
47 46 exlimdvv ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( ∃ 𝑥 ∃ 𝑦 ( ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) → ( 𝐴 ∪ 𝐶 ) ≼ ( 𝐵 ∪ 𝐷 ) ) )
48 19 47 syl5bir ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( ( ∃ 𝑥 ( 𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ∧ ∃ 𝑦 ( ( 𝐶 ∖ 𝐴 ) ≈ 𝑦 ∧ 𝑦 ⊆ 𝐷 ) ) → ( 𝐴 ∪ 𝐶 ) ≼ ( 𝐵 ∪ 𝐷 ) ) )
49 18 48 mpd ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐴 ∪ 𝐶 ) ≼ ( 𝐵 ∪ 𝐷 ) )