Step | Hyp | Ref
| Expression |
1 | | sdom0 8092 |
. . . . 5
⊢ ¬
𝐴 ≺
∅ |
2 | | breq2 4657 |
. . . . 5
⊢ (𝐵 = ∅ → (𝐴 ≺ 𝐵 ↔ 𝐴 ≺ ∅)) |
3 | 1, 2 | mtbiri 317 |
. . . 4
⊢ (𝐵 = ∅ → ¬ 𝐴 ≺ 𝐵) |
4 | 3 | con2i 134 |
. . 3
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐵 = ∅) |
5 | | neq0 3930 |
. . 3
⊢ (¬
𝐵 = ∅ ↔
∃𝑧 𝑧 ∈ 𝐵) |
6 | 4, 5 | sylib 208 |
. 2
⊢ (𝐴 ≺ 𝐵 → ∃𝑧 𝑧 ∈ 𝐵) |
7 | | domdifsn 8043 |
. . . . 5
⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ (𝐵 ∖ {𝑧})) |
8 | 7 | adantr 481 |
. . . 4
⊢ ((𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵) → 𝐴 ≼ (𝐵 ∖ {𝑧})) |
9 | | vex 3203 |
. . . . . . 7
⊢ 𝑧 ∈ V |
10 | | en2sn 8037 |
. . . . . . 7
⊢ ((𝐶 ∈ V ∧ 𝑧 ∈ V) → {𝐶} ≈ {𝑧}) |
11 | 9, 10 | mpan2 707 |
. . . . . 6
⊢ (𝐶 ∈ V → {𝐶} ≈ {𝑧}) |
12 | | endom 7982 |
. . . . . 6
⊢ ({𝐶} ≈ {𝑧} → {𝐶} ≼ {𝑧}) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ (𝐶 ∈ V → {𝐶} ≼ {𝑧}) |
14 | | snprc 4253 |
. . . . . . 7
⊢ (¬
𝐶 ∈ V ↔ {𝐶} = ∅) |
15 | 14 | biimpi 206 |
. . . . . 6
⊢ (¬
𝐶 ∈ V → {𝐶} = ∅) |
16 | | snex 4908 |
. . . . . . 7
⊢ {𝑧} ∈ V |
17 | 16 | 0dom 8090 |
. . . . . 6
⊢ ∅
≼ {𝑧} |
18 | 15, 17 | syl6eqbr 4692 |
. . . . 5
⊢ (¬
𝐶 ∈ V → {𝐶} ≼ {𝑧}) |
19 | 13, 18 | pm2.61i 176 |
. . . 4
⊢ {𝐶} ≼ {𝑧} |
20 | | incom 3805 |
. . . . . 6
⊢ ((𝐵 ∖ {𝑧}) ∩ {𝑧}) = ({𝑧} ∩ (𝐵 ∖ {𝑧})) |
21 | | disjdif 4040 |
. . . . . 6
⊢ ({𝑧} ∩ (𝐵 ∖ {𝑧})) = ∅ |
22 | 20, 21 | eqtri 2644 |
. . . . 5
⊢ ((𝐵 ∖ {𝑧}) ∩ {𝑧}) = ∅ |
23 | | undom 8048 |
. . . . 5
⊢ (((𝐴 ≼ (𝐵 ∖ {𝑧}) ∧ {𝐶} ≼ {𝑧}) ∧ ((𝐵 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (𝐴 ∪ {𝐶}) ≼ ((𝐵 ∖ {𝑧}) ∪ {𝑧})) |
24 | 22, 23 | mpan2 707 |
. . . 4
⊢ ((𝐴 ≼ (𝐵 ∖ {𝑧}) ∧ {𝐶} ≼ {𝑧}) → (𝐴 ∪ {𝐶}) ≼ ((𝐵 ∖ {𝑧}) ∪ {𝑧})) |
25 | 8, 19, 24 | sylancl 694 |
. . 3
⊢ ((𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝐴 ∪ {𝐶}) ≼ ((𝐵 ∖ {𝑧}) ∪ {𝑧})) |
26 | | uncom 3757 |
. . . 4
⊢ ((𝐵 ∖ {𝑧}) ∪ {𝑧}) = ({𝑧} ∪ (𝐵 ∖ {𝑧})) |
27 | | simpr 477 |
. . . . . 6
⊢ ((𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) |
28 | 27 | snssd 4340 |
. . . . 5
⊢ ((𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵) → {𝑧} ⊆ 𝐵) |
29 | | undif 4049 |
. . . . 5
⊢ ({𝑧} ⊆ 𝐵 ↔ ({𝑧} ∪ (𝐵 ∖ {𝑧})) = 𝐵) |
30 | 28, 29 | sylib 208 |
. . . 4
⊢ ((𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵) → ({𝑧} ∪ (𝐵 ∖ {𝑧})) = 𝐵) |
31 | 26, 30 | syl5eq 2668 |
. . 3
⊢ ((𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝐵 ∖ {𝑧}) ∪ {𝑧}) = 𝐵) |
32 | 25, 31 | breqtrd 4679 |
. 2
⊢ ((𝐴 ≺ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝐴 ∪ {𝐶}) ≼ 𝐵) |
33 | 6, 32 | exlimddv 1863 |
1
⊢ (𝐴 ≺ 𝐵 → (𝐴 ∪ {𝐶}) ≼ 𝐵) |