Proof of Theorem brdom3
| Step | Hyp | Ref
| Expression |
| 1 | | reldom 8991 |
. . . . . . . . 9
⊢ Rel
≼ |
| 2 | 1 | brrelex1i 5741 |
. . . . . . . 8
⊢ (𝐴 ≼ 𝐵 → 𝐴 ∈ V) |
| 3 | | 0sdomg 9144 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝐴 ≼ 𝐵 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 5 | | df-ne 2941 |
. . . . . . 7
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) |
| 6 | 4, 5 | bitrdi 287 |
. . . . . 6
⊢ (𝐴 ≼ 𝐵 → (∅ ≺ 𝐴 ↔ ¬ 𝐴 = ∅)) |
| 7 | 6 | biimpar 477 |
. . . . 5
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 = ∅) → ∅ ≺ 𝐴) |
| 8 | | fodomr 9168 |
. . . . . 6
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ 𝐵) → ∃𝑓 𝑓:𝐵–onto→𝐴) |
| 9 | 8 | ancoms 458 |
. . . . 5
⊢ ((𝐴 ≼ 𝐵 ∧ ∅ ≺ 𝐴) → ∃𝑓 𝑓:𝐵–onto→𝐴) |
| 10 | 7, 9 | syldan 591 |
. . . 4
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 = ∅) → ∃𝑓 𝑓:𝐵–onto→𝐴) |
| 11 | | pm5.6 1004 |
. . . 4
⊢ (((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 = ∅) → ∃𝑓 𝑓:𝐵–onto→𝐴) ↔ (𝐴 ≼ 𝐵 → (𝐴 = ∅ ∨ ∃𝑓 𝑓:𝐵–onto→𝐴))) |
| 12 | 10, 11 | mpbi 230 |
. . 3
⊢ (𝐴 ≼ 𝐵 → (𝐴 = ∅ ∨ ∃𝑓 𝑓:𝐵–onto→𝐴)) |
| 13 | | br0 5192 |
. . . . . . . 8
⊢ ¬
𝑥∅𝑦 |
| 14 | 13 | nex 1800 |
. . . . . . 7
⊢ ¬
∃𝑦 𝑥∅𝑦 |
| 15 | | exmo 2542 |
. . . . . . 7
⊢
(∃𝑦 𝑥∅𝑦 ∨ ∃*𝑦 𝑥∅𝑦) |
| 16 | 14, 15 | mtpor 1770 |
. . . . . 6
⊢
∃*𝑦 𝑥∅𝑦 |
| 17 | 16 | ax-gen 1795 |
. . . . 5
⊢
∀𝑥∃*𝑦 𝑥∅𝑦 |
| 18 | | rzal 4509 |
. . . . 5
⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦∅𝑥) |
| 19 | | 0ex 5307 |
. . . . . 6
⊢ ∅
∈ V |
| 20 | | breq 5145 |
. . . . . . . . 9
⊢ (𝑓 = ∅ → (𝑥𝑓𝑦 ↔ 𝑥∅𝑦)) |
| 21 | 20 | mobidv 2549 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (∃*𝑦 𝑥𝑓𝑦 ↔ ∃*𝑦 𝑥∅𝑦)) |
| 22 | 21 | albidv 1920 |
. . . . . . 7
⊢ (𝑓 = ∅ → (∀𝑥∃*𝑦 𝑥𝑓𝑦 ↔ ∀𝑥∃*𝑦 𝑥∅𝑦)) |
| 23 | | breq 5145 |
. . . . . . . . 9
⊢ (𝑓 = ∅ → (𝑦𝑓𝑥 ↔ 𝑦∅𝑥)) |
| 24 | 23 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (∃𝑦 ∈ 𝐵 𝑦𝑓𝑥 ↔ ∃𝑦 ∈ 𝐵 𝑦∅𝑥)) |
| 25 | 24 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑓 = ∅ → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦∅𝑥)) |
| 26 | 22, 25 | anbi12d 632 |
. . . . . 6
⊢ (𝑓 = ∅ →
((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) ↔ (∀𝑥∃*𝑦 𝑥∅𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦∅𝑥))) |
| 27 | 19, 26 | spcev 3606 |
. . . . 5
⊢
((∀𝑥∃*𝑦 𝑥∅𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦∅𝑥) → ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
| 28 | 17, 18, 27 | sylancr 587 |
. . . 4
⊢ (𝐴 = ∅ → ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
| 29 | | fofun 6821 |
. . . . . . 7
⊢ (𝑓:𝐵–onto→𝐴 → Fun 𝑓) |
| 30 | | dffun6 6574 |
. . . . . . . 8
⊢ (Fun
𝑓 ↔ (Rel 𝑓 ∧ ∀𝑥∃*𝑦 𝑥𝑓𝑦)) |
| 31 | 30 | simprbi 496 |
. . . . . . 7
⊢ (Fun
𝑓 → ∀𝑥∃*𝑦 𝑥𝑓𝑦) |
| 32 | 29, 31 | syl 17 |
. . . . . 6
⊢ (𝑓:𝐵–onto→𝐴 → ∀𝑥∃*𝑦 𝑥𝑓𝑦) |
| 33 | | dffo4 7123 |
. . . . . . 7
⊢ (𝑓:𝐵–onto→𝐴 ↔ (𝑓:𝐵⟶𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
| 34 | 33 | simprbi 496 |
. . . . . 6
⊢ (𝑓:𝐵–onto→𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) |
| 35 | 32, 34 | jca 511 |
. . . . 5
⊢ (𝑓:𝐵–onto→𝐴 → (∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
| 36 | 35 | eximi 1835 |
. . . 4
⊢
(∃𝑓 𝑓:𝐵–onto→𝐴 → ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
| 37 | 28, 36 | jaoi 858 |
. . 3
⊢ ((𝐴 = ∅ ∨ ∃𝑓 𝑓:𝐵–onto→𝐴) → ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
| 38 | 12, 37 | syl 17 |
. 2
⊢ (𝐴 ≼ 𝐵 → ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
| 39 | | inss1 4237 |
. . . . . . . . . . 11
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝑓 |
| 40 | 39 | ssbri 5188 |
. . . . . . . . . 10
⊢ (𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦 → 𝑥𝑓𝑦) |
| 41 | 40 | moimi 2545 |
. . . . . . . . 9
⊢
(∃*𝑦 𝑥𝑓𝑦 → ∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) |
| 42 | 41 | alimi 1811 |
. . . . . . . 8
⊢
(∀𝑥∃*𝑦 𝑥𝑓𝑦 → ∀𝑥∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) |
| 43 | | relinxp 5824 |
. . . . . . . . 9
⊢ Rel
(𝑓 ∩ (𝐵 × 𝐴)) |
| 44 | | dffun6 6574 |
. . . . . . . . 9
⊢ (Fun
(𝑓 ∩ (𝐵 × 𝐴)) ↔ (Rel (𝑓 ∩ (𝐵 × 𝐴)) ∧ ∀𝑥∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
| 45 | 43, 44 | mpbiran 709 |
. . . . . . . 8
⊢ (Fun
(𝑓 ∩ (𝐵 × 𝐴)) ↔ ∀𝑥∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) |
| 46 | 42, 45 | sylibr 234 |
. . . . . . 7
⊢
(∀𝑥∃*𝑦 𝑥𝑓𝑦 → Fun (𝑓 ∩ (𝐵 × 𝐴))) |
| 47 | 46 | funfnd 6597 |
. . . . . 6
⊢
(∀𝑥∃*𝑦 𝑥𝑓𝑦 → (𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴))) |
| 48 | | rninxp 6199 |
. . . . . . 7
⊢ (ran
(𝑓 ∩ (𝐵 × 𝐴)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) |
| 49 | 48 | biimpri 228 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥 → ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴) |
| 50 | 47, 49 | anim12i 613 |
. . . . 5
⊢
((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → ((𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴)) |
| 51 | | df-fo 6567 |
. . . . 5
⊢ ((𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴 ↔ ((𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴)) |
| 52 | 50, 51 | sylibr 234 |
. . . 4
⊢
((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → (𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴) |
| 53 | | vex 3484 |
. . . . . . 7
⊢ 𝑓 ∈ V |
| 54 | 53 | inex1 5317 |
. . . . . 6
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ∈ V |
| 55 | 54 | dmex 7931 |
. . . . 5
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ∈ V |
| 56 | 55 | fodom 10563 |
. . . 4
⊢ ((𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴 → 𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴))) |
| 57 | | brdom3.2 |
. . . . . 6
⊢ 𝐵 ∈ V |
| 58 | | inss2 4238 |
. . . . . . . 8
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ⊆ (𝐵 × 𝐴) |
| 59 | | dmss 5913 |
. . . . . . . 8
⊢ ((𝑓 ∩ (𝐵 × 𝐴)) ⊆ (𝐵 × 𝐴) → dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ dom (𝐵 × 𝐴)) |
| 60 | 58, 59 | ax-mp 5 |
. . . . . . 7
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ dom (𝐵 × 𝐴) |
| 61 | | dmxpss 6191 |
. . . . . . 7
⊢ dom
(𝐵 × 𝐴) ⊆ 𝐵 |
| 62 | 60, 61 | sstri 3993 |
. . . . . 6
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐵 |
| 63 | | ssdomg 9040 |
. . . . . 6
⊢ (𝐵 ∈ V → (dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐵 → dom (𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵)) |
| 64 | 57, 62, 63 | mp2 9 |
. . . . 5
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵 |
| 65 | | domtr 9047 |
. . . . 5
⊢ ((𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ dom (𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵) → 𝐴 ≼ 𝐵) |
| 66 | 64, 65 | mpan2 691 |
. . . 4
⊢ (𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴)) → 𝐴 ≼ 𝐵) |
| 67 | 52, 56, 66 | 3syl 18 |
. . 3
⊢
((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ 𝐵) |
| 68 | 67 | exlimiv 1930 |
. 2
⊢
(∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ 𝐵) |
| 69 | 38, 68 | impbii 209 |
1
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |