Metamath Proof Explorer

Theorem domunsn

Description: Dominance over a set with one element added. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion domunsn ⊢ A ≺ B → A ∪ C ≼ B

Proof

Step Hyp Ref Expression
1 sdom0 ⊢ ¬ A ≺ ∅
2 breq2 ⊢ B = ∅ → A ≺ B ↔ A ≺ ∅
3 1 2 mtbiri ⊢ B = ∅ → ¬ A ≺ B
4 3 con2i ⊢ A ≺ B → ¬ B = ∅
5 neq0 ⊢ ¬ B = ∅ ↔ ∃ z z ∈ B
6 4 5 sylib ⊢ A ≺ B → ∃ z z ∈ B
7 domdifsn ⊢ A ≺ B → A ≼ B ∖ z
8 7 adantr ⊢ A ≺ B ∧ z ∈ B → A ≼ B ∖ z
9 en2sn ⊢ C ∈ V ∧ z ∈ V → C ≈ z
10 9 elvd ⊢ C ∈ V → C ≈ z
11 endom ⊢ C ≈ z → C ≼ z
12 10 11 syl ⊢ C ∈ V → C ≼ z
13 snprc ⊢ ¬ C ∈ V ↔ C = ∅
14 13 biimpi ⊢ ¬ C ∈ V → C = ∅
15 snex ⊢ z ∈ V
16 15 0dom ⊢ ∅ ≼ z
17 14 16 eqbrtrdi ⊢ ¬ C ∈ V → C ≼ z
18 12 17 pm2.61i ⊢ C ≼ z
19 disjdifr ⊢ B ∖ z ∩ z = ∅
20 undom ⊢ A ≼ B ∖ z ∧ C ≼ z ∧ B ∖ z ∩ z = ∅ → A ∪ C ≼ B ∖ z ∪ z
21 19 20 mpan2 ⊢ A ≼ B ∖ z ∧ C ≼ z → A ∪ C ≼ B ∖ z ∪ z
22 8 18 21 sylancl ⊢ A ≺ B ∧ z ∈ B → A ∪ C ≼ B ∖ z ∪ z
23 uncom ⊢ B ∖ z ∪ z = z ∪ B ∖ z
24 simpr ⊢ A ≺ B ∧ z ∈ B → z ∈ B
25 24 snssd ⊢ A ≺ B ∧ z ∈ B → z ⊆ B
26 undif ⊢ z ⊆ B ↔ z ∪ B ∖ z = B
27 25 26 sylib ⊢ A ≺ B ∧ z ∈ B → z ∪ B ∖ z = B
28 23 27 eqtrid ⊢ A ≺ B ∧ z ∈ B → B ∖ z ∪ z = B
29 22 28 breqtrd ⊢ A ≺ B ∧ z ∈ B → A ∪ C ≼ B
30 6 29 exlimddv ⊢ A ≺ B → A ∪ C ≼ B