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) Avoid ax-pow . (Revised by BTernaryTau, 4-Dec-2024)

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

Proof

Step Hyp Ref Expression
1 undif2 ⊢ ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) = ( 𝐴 ∪ 𝐶 )
2 reldom ⊢ Rel ≼
3 2 brrelex2i ⊢ ( 𝐴 ≼ 𝐵 → 𝐵 ∈ V )
4 2 brrelex2i ⊢ ( 𝐶 ≼ 𝐷 → 𝐷 ∈ V )
5 unexg ⊢ ( ( 𝐵 ∈ V ∧ 𝐷 ∈ V ) → ( 𝐵 ∪ 𝐷 ) ∈ V )
6 3 4 5 syl2an ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) → ( 𝐵 ∪ 𝐷 ) ∈ V )
7 6 adantr ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐵 ∪ 𝐷 ) ∈ V )
8 brdomi ⊢ ( 𝐴 ≼ 𝐵 → ∃ 𝑥 𝑥 : 𝐴 –1-1→ 𝐵 )
9 brdomi ⊢ ( 𝐶 ≼ 𝐷 → ∃ 𝑦 𝑦 : 𝐶 –1-1→ 𝐷 )
10 exdistrv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 : 𝐴 –1-1→ 𝐵 ∧ 𝑦 : 𝐶 –1-1→ 𝐷 ) ↔ ( ∃ 𝑥 𝑥 : 𝐴 –1-1→ 𝐵 ∧ ∃ 𝑦 𝑦 : 𝐶 –1-1→ 𝐷 ) )
11 disjdif ⊢ ( 𝐴 ∩ ( 𝐶 ∖ 𝐴 ) ) = ∅
12 difss ⊢ ( 𝐶 ∖ 𝐴 ) ⊆ 𝐶
13 f1ssres ⊢ ( ( 𝑦 : 𝐶 –1-1→ 𝐷 ∧ ( 𝐶 ∖ 𝐴 ) ⊆ 𝐶 ) → ( 𝑦 ↾ ( 𝐶 ∖ 𝐴 ) ) : ( 𝐶 ∖ 𝐴 ) –1-1→ 𝐷 )
14 12 13 mpan2 ⊢ ( 𝑦 : 𝐶 –1-1→ 𝐷 → ( 𝑦 ↾ ( 𝐶 ∖ 𝐴 ) ) : ( 𝐶 ∖ 𝐴 ) –1-1→ 𝐷 )
15 f1un ⊢ ( ( ( 𝑥 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑦 ↾ ( 𝐶 ∖ 𝐴 ) ) : ( 𝐶 ∖ 𝐴 ) –1-1→ 𝐷 ) ∧ ( ( 𝐴 ∩ ( 𝐶 ∖ 𝐴 ) ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ) → ( 𝑥 ∪ ( 𝑦 ↾ ( 𝐶 ∖ 𝐴 ) ) ) : ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) –1-1→ ( 𝐵 ∪ 𝐷 ) )
16 14 15 sylanl2 ⊢ ( ( ( 𝑥 : 𝐴 –1-1→ 𝐵 ∧ 𝑦 : 𝐶 –1-1→ 𝐷 ) ∧ ( ( 𝐴 ∩ ( 𝐶 ∖ 𝐴 ) ) = ∅ ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) ) → ( 𝑥 ∪ ( 𝑦 ↾ ( 𝐶 ∖ 𝐴 ) ) ) : ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) –1-1→ ( 𝐵 ∪ 𝐷 ) )
17 11 16 mpanr1 ⊢ ( ( ( 𝑥 : 𝐴 –1-1→ 𝐵 ∧ 𝑦 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝑥 ∪ ( 𝑦 ↾ ( 𝐶 ∖ 𝐴 ) ) ) : ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) –1-1→ ( 𝐵 ∪ 𝐷 ) )
18 vex ⊢ 𝑥 ∈ V
19 vex ⊢ 𝑦 ∈ V
20 19 resex ⊢ ( 𝑦 ↾ ( 𝐶 ∖ 𝐴 ) ) ∈ V
21 18 20 unex ⊢ ( 𝑥 ∪ ( 𝑦 ↾ ( 𝐶 ∖ 𝐴 ) ) ) ∈ V
22 f1dom3g ⊢ ( ( ( 𝑥 ∪ ( 𝑦 ↾ ( 𝐶 ∖ 𝐴 ) ) ) ∈ V ∧ ( 𝐵 ∪ 𝐷 ) ∈ V ∧ ( 𝑥 ∪ ( 𝑦 ↾ ( 𝐶 ∖ 𝐴 ) ) ) : ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) –1-1→ ( 𝐵 ∪ 𝐷 ) ) → ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) ≼ ( 𝐵 ∪ 𝐷 ) )
23 21 22 mp3an1 ⊢ ( ( ( 𝐵 ∪ 𝐷 ) ∈ V ∧ ( 𝑥 ∪ ( 𝑦 ↾ ( 𝐶 ∖ 𝐴 ) ) ) : ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) –1-1→ ( 𝐵 ∪ 𝐷 ) ) → ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) ≼ ( 𝐵 ∪ 𝐷 ) )
24 23 expcom ⊢ ( ( 𝑥 ∪ ( 𝑦 ↾ ( 𝐶 ∖ 𝐴 ) ) ) : ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) –1-1→ ( 𝐵 ∪ 𝐷 ) → ( ( 𝐵 ∪ 𝐷 ) ∈ V → ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) ≼ ( 𝐵 ∪ 𝐷 ) ) )
25 17 24 syl ⊢ ( ( ( 𝑥 : 𝐴 –1-1→ 𝐵 ∧ 𝑦 : 𝐶 –1-1→ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( ( 𝐵 ∪ 𝐷 ) ∈ V → ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) ≼ ( 𝐵 ∪ 𝐷 ) ) )
26 25 ex ⊢ ( ( 𝑥 : 𝐴 –1-1→ 𝐵 ∧ 𝑦 : 𝐶 –1-1→ 𝐷 ) → ( ( 𝐵 ∩ 𝐷 ) = ∅ → ( ( 𝐵 ∪ 𝐷 ) ∈ V → ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) ≼ ( 𝐵 ∪ 𝐷 ) ) ) )
27 26 exlimivv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 : 𝐴 –1-1→ 𝐵 ∧ 𝑦 : 𝐶 –1-1→ 𝐷 ) → ( ( 𝐵 ∩ 𝐷 ) = ∅ → ( ( 𝐵 ∪ 𝐷 ) ∈ V → ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) ≼ ( 𝐵 ∪ 𝐷 ) ) ) )
28 10 27 sylbir ⊢ ( ( ∃ 𝑥 𝑥 : 𝐴 –1-1→ 𝐵 ∧ ∃ 𝑦 𝑦 : 𝐶 –1-1→ 𝐷 ) → ( ( 𝐵 ∩ 𝐷 ) = ∅ → ( ( 𝐵 ∪ 𝐷 ) ∈ V → ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) ≼ ( 𝐵 ∪ 𝐷 ) ) ) )
29 8 9 28 syl2an ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) → ( ( 𝐵 ∩ 𝐷 ) = ∅ → ( ( 𝐵 ∪ 𝐷 ) ∈ V → ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) ≼ ( 𝐵 ∪ 𝐷 ) ) ) )
30 29 imp ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( ( 𝐵 ∪ 𝐷 ) ∈ V → ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) ≼ ( 𝐵 ∪ 𝐷 ) ) )
31 7 30 mpd ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐴 ∪ ( 𝐶 ∖ 𝐴 ) ) ≼ ( 𝐵 ∪ 𝐷 ) )
32 1 31 eqbrtrrid ⊢ ( ( ( 𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷 ) ∧ ( 𝐵 ∩ 𝐷 ) = ∅ ) → ( 𝐴 ∪ 𝐶 ) ≼ ( 𝐵 ∪ 𝐷 ) )