Step | Hyp | Ref
| Expression |
1 | | undif2 4410 |
. 2
⊢ (𝐴 ∪ (𝐶 ∖ 𝐴)) = (𝐴 ∪ 𝐶) |
2 | | reldom 8739 |
. . . . . 6
⊢ Rel
≼ |
3 | 2 | brrelex2i 5644 |
. . . . 5
⊢ (𝐴 ≼ 𝐵 → 𝐵 ∈ V) |
4 | 2 | brrelex2i 5644 |
. . . . 5
⊢ (𝐶 ≼ 𝐷 → 𝐷 ∈ V) |
5 | | unexg 7599 |
. . . . 5
⊢ ((𝐵 ∈ V ∧ 𝐷 ∈ V) → (𝐵 ∪ 𝐷) ∈ V) |
6 | 3, 4, 5 | syl2an 596 |
. . . 4
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) → (𝐵 ∪ 𝐷) ∈ V) |
7 | 6 | adantr 481 |
. . 3
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐵 ∪ 𝐷) ∈ V) |
8 | | brdomi 8748 |
. . . . 5
⊢ (𝐴 ≼ 𝐵 → ∃𝑥 𝑥:𝐴–1-1→𝐵) |
9 | | brdomi 8748 |
. . . . 5
⊢ (𝐶 ≼ 𝐷 → ∃𝑦 𝑦:𝐶–1-1→𝐷) |
10 | | exdistrv 1959 |
. . . . . 6
⊢
(∃𝑥∃𝑦(𝑥:𝐴–1-1→𝐵 ∧ 𝑦:𝐶–1-1→𝐷) ↔ (∃𝑥 𝑥:𝐴–1-1→𝐵 ∧ ∃𝑦 𝑦:𝐶–1-1→𝐷)) |
11 | | disjdif 4405 |
. . . . . . . . . 10
⊢ (𝐴 ∩ (𝐶 ∖ 𝐴)) = ∅ |
12 | | difss 4066 |
. . . . . . . . . . . 12
⊢ (𝐶 ∖ 𝐴) ⊆ 𝐶 |
13 | | f1ssres 6678 |
. . . . . . . . . . . 12
⊢ ((𝑦:𝐶–1-1→𝐷 ∧ (𝐶 ∖ 𝐴) ⊆ 𝐶) → (𝑦 ↾ (𝐶 ∖ 𝐴)):(𝐶 ∖ 𝐴)–1-1→𝐷) |
14 | 12, 13 | mpan2 688 |
. . . . . . . . . . 11
⊢ (𝑦:𝐶–1-1→𝐷 → (𝑦 ↾ (𝐶 ∖ 𝐴)):(𝐶 ∖ 𝐴)–1-1→𝐷) |
15 | | f1un 6736 |
. . . . . . . . . . 11
⊢ (((𝑥:𝐴–1-1→𝐵 ∧ (𝑦 ↾ (𝐶 ∖ 𝐴)):(𝐶 ∖ 𝐴)–1-1→𝐷) ∧ ((𝐴 ∩ (𝐶 ∖ 𝐴)) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))):(𝐴 ∪ (𝐶 ∖ 𝐴))–1-1→(𝐵 ∪ 𝐷)) |
16 | 14, 15 | sylanl2 678 |
. . . . . . . . . 10
⊢ (((𝑥:𝐴–1-1→𝐵 ∧ 𝑦:𝐶–1-1→𝐷) ∧ ((𝐴 ∩ (𝐶 ∖ 𝐴)) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))):(𝐴 ∪ (𝐶 ∖ 𝐴))–1-1→(𝐵 ∪ 𝐷)) |
17 | 11, 16 | mpanr1 700 |
. . . . . . . . 9
⊢ (((𝑥:𝐴–1-1→𝐵 ∧ 𝑦:𝐶–1-1→𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))):(𝐴 ∪ (𝐶 ∖ 𝐴))–1-1→(𝐵 ∪ 𝐷)) |
18 | | vex 3436 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
19 | | vex 3436 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
20 | 19 | resex 5939 |
. . . . . . . . . . . 12
⊢ (𝑦 ↾ (𝐶 ∖ 𝐴)) ∈ V |
21 | 18, 20 | unex 7596 |
. . . . . . . . . . 11
⊢ (𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))) ∈ V |
22 | | f1dom3g 8755 |
. . . . . . . . . . 11
⊢ (((𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))) ∈ V ∧ (𝐵 ∪ 𝐷) ∈ V ∧ (𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))):(𝐴 ∪ (𝐶 ∖ 𝐴))–1-1→(𝐵 ∪ 𝐷)) → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷)) |
23 | 21, 22 | mp3an1 1447 |
. . . . . . . . . 10
⊢ (((𝐵 ∪ 𝐷) ∈ V ∧ (𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))):(𝐴 ∪ (𝐶 ∖ 𝐴))–1-1→(𝐵 ∪ 𝐷)) → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷)) |
24 | 23 | expcom 414 |
. . . . . . . . 9
⊢ ((𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))):(𝐴 ∪ (𝐶 ∖ 𝐴))–1-1→(𝐵 ∪ 𝐷) → ((𝐵 ∪ 𝐷) ∈ V → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷))) |
25 | 17, 24 | syl 17 |
. . . . . . . 8
⊢ (((𝑥:𝐴–1-1→𝐵 ∧ 𝑦:𝐶–1-1→𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → ((𝐵 ∪ 𝐷) ∈ V → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷))) |
26 | 25 | ex 413 |
. . . . . . 7
⊢ ((𝑥:𝐴–1-1→𝐵 ∧ 𝑦:𝐶–1-1→𝐷) → ((𝐵 ∩ 𝐷) = ∅ → ((𝐵 ∪ 𝐷) ∈ V → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷)))) |
27 | 26 | exlimivv 1935 |
. . . . . 6
⊢
(∃𝑥∃𝑦(𝑥:𝐴–1-1→𝐵 ∧ 𝑦:𝐶–1-1→𝐷) → ((𝐵 ∩ 𝐷) = ∅ → ((𝐵 ∪ 𝐷) ∈ V → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷)))) |
28 | 10, 27 | sylbir 234 |
. . . . 5
⊢
((∃𝑥 𝑥:𝐴–1-1→𝐵 ∧ ∃𝑦 𝑦:𝐶–1-1→𝐷) → ((𝐵 ∩ 𝐷) = ∅ → ((𝐵 ∪ 𝐷) ∈ V → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷)))) |
29 | 8, 9, 28 | syl2an 596 |
. . . 4
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) → ((𝐵 ∩ 𝐷) = ∅ → ((𝐵 ∪ 𝐷) ∈ V → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷)))) |
30 | 29 | imp 407 |
. . 3
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → ((𝐵 ∪ 𝐷) ∈ V → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷))) |
31 | 7, 30 | mpd 15 |
. 2
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷)) |
32 | 1, 31 | eqbrtrrid 5110 |
1
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼ (𝐵 ∪ 𝐷)) |