| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sdom0 9148 | . . . . 5
⊢  ¬
𝐴 ≺
∅ | 
| 2 |  | breq2 5147 | . . . . 5
⊢ (𝐵 = ∅ → (𝐴 ≺ 𝐵 ↔ 𝐴 ≺ ∅)) | 
| 3 | 1, 2 | mtbiri 327 | . . . 4
⊢ (𝐵 = ∅ → ¬ 𝐴 ≺ 𝐵) | 
| 4 | 3 | con2i 139 | . . 3
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐵 = ∅) | 
| 5 |  | neq0 4352 | . . 3
⊢ (¬
𝐵 = ∅ ↔
∃𝑧 𝑧 ∈ 𝐵) | 
| 6 | 4, 5 | sylib 218 | . 2
⊢ (𝐴 ≺ 𝐵 → ∃𝑧 𝑧 ∈ 𝐵) | 
| 7 |  | domdifsn 9094 | . . . . 5
⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ (𝐵 ∖ {𝑧})) | 
| 8 | 7 | adantr 480 | . . . 4
⊢ ((𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵) → 𝐴 ≼ (𝐵 ∖ {𝑧})) | 
| 9 |  | en2sn 9081 | . . . . . . 7
⊢ ((𝐶 ∈ V ∧ 𝑧 ∈ V) → {𝐶} ≈ {𝑧}) | 
| 10 | 9 | elvd 3486 | . . . . . 6
⊢ (𝐶 ∈ V → {𝐶} ≈ {𝑧}) | 
| 11 |  | endom 9019 | . . . . . 6
⊢ ({𝐶} ≈ {𝑧} → {𝐶} ≼ {𝑧}) | 
| 12 | 10, 11 | syl 17 | . . . . 5
⊢ (𝐶 ∈ V → {𝐶} ≼ {𝑧}) | 
| 13 |  | snprc 4717 | . . . . . . 7
⊢ (¬
𝐶 ∈ V ↔ {𝐶} = ∅) | 
| 14 | 13 | biimpi 216 | . . . . . 6
⊢ (¬
𝐶 ∈ V → {𝐶} = ∅) | 
| 15 |  | vsnex 5434 | . . . . . . 7
⊢ {𝑧} ∈ V | 
| 16 | 15 | 0dom 9146 | . . . . . 6
⊢ ∅
≼ {𝑧} | 
| 17 | 14, 16 | eqbrtrdi 5182 | . . . . 5
⊢ (¬
𝐶 ∈ V → {𝐶} ≼ {𝑧}) | 
| 18 | 12, 17 | pm2.61i 182 | . . . 4
⊢ {𝐶} ≼ {𝑧} | 
| 19 |  | disjdifr 4473 | . . . . 5
⊢ ((𝐵 ∖ {𝑧}) ∩ {𝑧}) = ∅ | 
| 20 |  | undom 9099 | . . . . 5
⊢ (((𝐴 ≼ (𝐵 ∖ {𝑧}) ∧ {𝐶} ≼ {𝑧}) ∧ ((𝐵 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (𝐴 ∪ {𝐶}) ≼ ((𝐵 ∖ {𝑧}) ∪ {𝑧})) | 
| 21 | 19, 20 | mpan2 691 | . . . 4
⊢ ((𝐴 ≼ (𝐵 ∖ {𝑧}) ∧ {𝐶} ≼ {𝑧}) → (𝐴 ∪ {𝐶}) ≼ ((𝐵 ∖ {𝑧}) ∪ {𝑧})) | 
| 22 | 8, 18, 21 | sylancl 586 | . . 3
⊢ ((𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝐴 ∪ {𝐶}) ≼ ((𝐵 ∖ {𝑧}) ∪ {𝑧})) | 
| 23 |  | uncom 4158 | . . . 4
⊢ ((𝐵 ∖ {𝑧}) ∪ {𝑧}) = ({𝑧} ∪ (𝐵 ∖ {𝑧})) | 
| 24 |  | simpr 484 | . . . . . 6
⊢ ((𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) | 
| 25 | 24 | snssd 4809 | . . . . 5
⊢ ((𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵) → {𝑧} ⊆ 𝐵) | 
| 26 |  | undif 4482 | . . . . 5
⊢ ({𝑧} ⊆ 𝐵 ↔ ({𝑧} ∪ (𝐵 ∖ {𝑧})) = 𝐵) | 
| 27 | 25, 26 | sylib 218 | . . . 4
⊢ ((𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵) → ({𝑧} ∪ (𝐵 ∖ {𝑧})) = 𝐵) | 
| 28 | 23, 27 | eqtrid 2789 | . . 3
⊢ ((𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝐵 ∖ {𝑧}) ∪ {𝑧}) = 𝐵) | 
| 29 | 22, 28 | breqtrd 5169 | . 2
⊢ ((𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝐴 ∪ {𝐶}) ≼ 𝐵) | 
| 30 | 6, 29 | exlimddv 1935 | 1
⊢ (𝐴 ≺ 𝐵 → (𝐴 ∪ {𝐶}) ≼ 𝐵) |