| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | undif2 4476 | . 2
⊢ (𝐴 ∪ (𝐶 ∖ 𝐴)) = (𝐴 ∪ 𝐶) | 
| 2 |  | reldom 8992 | . . . . . 6
⊢ Rel
≼ | 
| 3 | 2 | brrelex2i 5741 | . . . . 5
⊢ (𝐴 ≼ 𝐵 → 𝐵 ∈ V) | 
| 4 | 2 | brrelex2i 5741 | . . . . 5
⊢ (𝐶 ≼ 𝐷 → 𝐷 ∈ V) | 
| 5 |  | unexg 7764 | . . . . 5
⊢ ((𝐵 ∈ V ∧ 𝐷 ∈ V) → (𝐵 ∪ 𝐷) ∈ V) | 
| 6 | 3, 4, 5 | syl2an 596 | . . . 4
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) → (𝐵 ∪ 𝐷) ∈ V) | 
| 7 | 6 | adantr 480 | . . 3
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐵 ∪ 𝐷) ∈ V) | 
| 8 |  | brdomi 9000 | . . . . 5
⊢ (𝐴 ≼ 𝐵 → ∃𝑥 𝑥:𝐴–1-1→𝐵) | 
| 9 |  | brdomi 9000 | . . . . 5
⊢ (𝐶 ≼ 𝐷 → ∃𝑦 𝑦:𝐶–1-1→𝐷) | 
| 10 |  | exdistrv 1954 | . . . . . 6
⊢
(∃𝑥∃𝑦(𝑥:𝐴–1-1→𝐵 ∧ 𝑦:𝐶–1-1→𝐷) ↔ (∃𝑥 𝑥:𝐴–1-1→𝐵 ∧ ∃𝑦 𝑦:𝐶–1-1→𝐷)) | 
| 11 |  | disjdif 4471 | . . . . . . . . . 10
⊢ (𝐴 ∩ (𝐶 ∖ 𝐴)) = ∅ | 
| 12 |  | difss 4135 | . . . . . . . . . . . 12
⊢ (𝐶 ∖ 𝐴) ⊆ 𝐶 | 
| 13 |  | f1ssres 6810 | . . . . . . . . . . . 12
⊢ ((𝑦:𝐶–1-1→𝐷 ∧ (𝐶 ∖ 𝐴) ⊆ 𝐶) → (𝑦 ↾ (𝐶 ∖ 𝐴)):(𝐶 ∖ 𝐴)–1-1→𝐷) | 
| 14 | 12, 13 | mpan2 691 | . . . . . . . . . . 11
⊢ (𝑦:𝐶–1-1→𝐷 → (𝑦 ↾ (𝐶 ∖ 𝐴)):(𝐶 ∖ 𝐴)–1-1→𝐷) | 
| 15 |  | f1un 6867 | . . . . . . . . . . 11
⊢ (((𝑥:𝐴–1-1→𝐵 ∧ (𝑦 ↾ (𝐶 ∖ 𝐴)):(𝐶 ∖ 𝐴)–1-1→𝐷) ∧ ((𝐴 ∩ (𝐶 ∖ 𝐴)) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))):(𝐴 ∪ (𝐶 ∖ 𝐴))–1-1→(𝐵 ∪ 𝐷)) | 
| 16 | 14, 15 | sylanl2 681 | . . . . . . . . . 10
⊢ (((𝑥:𝐴–1-1→𝐵 ∧ 𝑦:𝐶–1-1→𝐷) ∧ ((𝐴 ∩ (𝐶 ∖ 𝐴)) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))):(𝐴 ∪ (𝐶 ∖ 𝐴))–1-1→(𝐵 ∪ 𝐷)) | 
| 17 | 11, 16 | mpanr1 703 | . . . . . . . . 9
⊢ (((𝑥:𝐴–1-1→𝐵 ∧ 𝑦:𝐶–1-1→𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))):(𝐴 ∪ (𝐶 ∖ 𝐴))–1-1→(𝐵 ∪ 𝐷)) | 
| 18 |  | vex 3483 | . . . . . . . . . . . 12
⊢ 𝑥 ∈ V | 
| 19 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑦 ∈ V | 
| 20 | 19 | resex 6046 | . . . . . . . . . . . 12
⊢ (𝑦 ↾ (𝐶 ∖ 𝐴)) ∈ V | 
| 21 | 18, 20 | unex 7765 | . . . . . . . . . . 11
⊢ (𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))) ∈ V | 
| 22 |  | f1dom3g 9009 | . . . . . . . . . . 11
⊢ (((𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))) ∈ V ∧ (𝐵 ∪ 𝐷) ∈ V ∧ (𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))):(𝐴 ∪ (𝐶 ∖ 𝐴))–1-1→(𝐵 ∪ 𝐷)) → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷)) | 
| 23 | 21, 22 | mp3an1 1449 | . . . . . . . . . 10
⊢ (((𝐵 ∪ 𝐷) ∈ V ∧ (𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))):(𝐴 ∪ (𝐶 ∖ 𝐴))–1-1→(𝐵 ∪ 𝐷)) → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷)) | 
| 24 | 23 | expcom 413 | . . . . . . . . 9
⊢ ((𝑥 ∪ (𝑦 ↾ (𝐶 ∖ 𝐴))):(𝐴 ∪ (𝐶 ∖ 𝐴))–1-1→(𝐵 ∪ 𝐷) → ((𝐵 ∪ 𝐷) ∈ V → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷))) | 
| 25 | 17, 24 | syl 17 | . . . . . . . 8
⊢ (((𝑥:𝐴–1-1→𝐵 ∧ 𝑦:𝐶–1-1→𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → ((𝐵 ∪ 𝐷) ∈ V → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷))) | 
| 26 | 25 | ex 412 | . . . . . . 7
⊢ ((𝑥:𝐴–1-1→𝐵 ∧ 𝑦:𝐶–1-1→𝐷) → ((𝐵 ∩ 𝐷) = ∅ → ((𝐵 ∪ 𝐷) ∈ V → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷)))) | 
| 27 | 26 | exlimivv 1931 | . . . . . 6
⊢
(∃𝑥∃𝑦(𝑥:𝐴–1-1→𝐵 ∧ 𝑦:𝐶–1-1→𝐷) → ((𝐵 ∩ 𝐷) = ∅ → ((𝐵 ∪ 𝐷) ∈ V → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷)))) | 
| 28 | 10, 27 | sylbir 235 | . . . . 5
⊢
((∃𝑥 𝑥:𝐴–1-1→𝐵 ∧ ∃𝑦 𝑦:𝐶–1-1→𝐷) → ((𝐵 ∩ 𝐷) = ∅ → ((𝐵 ∪ 𝐷) ∈ V → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷)))) | 
| 29 | 8, 9, 28 | syl2an 596 | . . . 4
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) → ((𝐵 ∩ 𝐷) = ∅ → ((𝐵 ∪ 𝐷) ∈ V → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷)))) | 
| 30 | 29 | imp 406 | . . 3
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → ((𝐵 ∪ 𝐷) ∈ V → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷))) | 
| 31 | 7, 30 | mpd 15 | . 2
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ (𝐶 ∖ 𝐴)) ≼ (𝐵 ∪ 𝐷)) | 
| 32 | 1, 31 | eqbrtrrid 5178 | 1
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼ (𝐵 ∪ 𝐷)) |