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