Proof of Theorem brdom3
Step | Hyp | Ref
| Expression |
1 | | reldom 7847 |
. . . . . . . . 9
⊢ Rel
≼ |
2 | 1 | brrelexi 5082 |
. . . . . . . 8
⊢ (𝐴 ≼ 𝐵 → 𝐴 ∈ V) |
3 | | 0sdomg 7974 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝐴 ≼ 𝐵 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
5 | | df-ne 2782 |
. . . . . . 7
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) |
6 | 4, 5 | syl6bb 275 |
. . . . . 6
⊢ (𝐴 ≼ 𝐵 → (∅ ≺ 𝐴 ↔ ¬ 𝐴 = ∅)) |
7 | 6 | biimpar 501 |
. . . . 5
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 = ∅) → ∅ ≺ 𝐴) |
8 | | fodomr 7996 |
. . . . . 6
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ 𝐵) → ∃𝑓 𝑓:𝐵–onto→𝐴) |
9 | 8 | ancoms 468 |
. . . . 5
⊢ ((𝐴 ≼ 𝐵 ∧ ∅ ≺ 𝐴) → ∃𝑓 𝑓:𝐵–onto→𝐴) |
10 | 7, 9 | syldan 486 |
. . . 4
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 = ∅) → ∃𝑓 𝑓:𝐵–onto→𝐴) |
11 | | pm5.6 949 |
. . . 4
⊢ (((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 = ∅) → ∃𝑓 𝑓:𝐵–onto→𝐴) ↔ (𝐴 ≼ 𝐵 → (𝐴 = ∅ ∨ ∃𝑓 𝑓:𝐵–onto→𝐴))) |
12 | 10, 11 | mpbi 219 |
. . 3
⊢ (𝐴 ≼ 𝐵 → (𝐴 = ∅ ∨ ∃𝑓 𝑓:𝐵–onto→𝐴)) |
13 | | br0 4631 |
. . . . . . . 8
⊢ ¬
𝑥∅𝑦 |
14 | 13 | nex 1722 |
. . . . . . 7
⊢ ¬
∃𝑦 𝑥∅𝑦 |
15 | | exmo 2483 |
. . . . . . 7
⊢
(∃𝑦 𝑥∅𝑦 ∨ ∃*𝑦 𝑥∅𝑦) |
16 | 14, 15 | mtpor 1686 |
. . . . . 6
⊢
∃*𝑦 𝑥∅𝑦 |
17 | 16 | ax-gen 1713 |
. . . . 5
⊢
∀𝑥∃*𝑦 𝑥∅𝑦 |
18 | | rzal 4025 |
. . . . 5
⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦∅𝑥) |
19 | | 0ex 4718 |
. . . . . 6
⊢ ∅
∈ V |
20 | | breq 4585 |
. . . . . . . . 9
⊢ (𝑓 = ∅ → (𝑥𝑓𝑦 ↔ 𝑥∅𝑦)) |
21 | 20 | mobidv 2479 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (∃*𝑦 𝑥𝑓𝑦 ↔ ∃*𝑦 𝑥∅𝑦)) |
22 | 21 | albidv 1836 |
. . . . . . 7
⊢ (𝑓 = ∅ → (∀𝑥∃*𝑦 𝑥𝑓𝑦 ↔ ∀𝑥∃*𝑦 𝑥∅𝑦)) |
23 | | breq 4585 |
. . . . . . . . 9
⊢ (𝑓 = ∅ → (𝑦𝑓𝑥 ↔ 𝑦∅𝑥)) |
24 | 23 | rexbidv 3034 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (∃𝑦 ∈ 𝐵 𝑦𝑓𝑥 ↔ ∃𝑦 ∈ 𝐵 𝑦∅𝑥)) |
25 | 24 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑓 = ∅ → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦∅𝑥)) |
26 | 22, 25 | anbi12d 743 |
. . . . . 6
⊢ (𝑓 = ∅ →
((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) ↔ (∀𝑥∃*𝑦 𝑥∅𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦∅𝑥))) |
27 | 19, 26 | spcev 3273 |
. . . . 5
⊢
((∀𝑥∃*𝑦 𝑥∅𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦∅𝑥) → ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
28 | 17, 18, 27 | sylancr 694 |
. . . 4
⊢ (𝐴 = ∅ → ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
29 | | fofun 6029 |
. . . . . . 7
⊢ (𝑓:𝐵–onto→𝐴 → Fun 𝑓) |
30 | | dffun6 5819 |
. . . . . . . 8
⊢ (Fun
𝑓 ↔ (Rel 𝑓 ∧ ∀𝑥∃*𝑦 𝑥𝑓𝑦)) |
31 | 30 | simprbi 479 |
. . . . . . 7
⊢ (Fun
𝑓 → ∀𝑥∃*𝑦 𝑥𝑓𝑦) |
32 | 29, 31 | syl 17 |
. . . . . 6
⊢ (𝑓:𝐵–onto→𝐴 → ∀𝑥∃*𝑦 𝑥𝑓𝑦) |
33 | | dffo4 6283 |
. . . . . . 7
⊢ (𝑓:𝐵–onto→𝐴 ↔ (𝑓:𝐵⟶𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
34 | 33 | simprbi 479 |
. . . . . 6
⊢ (𝑓:𝐵–onto→𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) |
35 | 32, 34 | jca 553 |
. . . . 5
⊢ (𝑓:𝐵–onto→𝐴 → (∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
36 | 35 | eximi 1752 |
. . . 4
⊢
(∃𝑓 𝑓:𝐵–onto→𝐴 → ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
37 | 28, 36 | jaoi 393 |
. . 3
⊢ ((𝐴 = ∅ ∨ ∃𝑓 𝑓:𝐵–onto→𝐴) → ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
38 | 12, 37 | syl 17 |
. 2
⊢ (𝐴 ≼ 𝐵 → ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
39 | | inss1 3795 |
. . . . . . . . . . 11
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝑓 |
40 | 39 | ssbri 4627 |
. . . . . . . . . 10
⊢ (𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦 → 𝑥𝑓𝑦) |
41 | 40 | moimi 2508 |
. . . . . . . . 9
⊢
(∃*𝑦 𝑥𝑓𝑦 → ∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) |
42 | 41 | alimi 1730 |
. . . . . . . 8
⊢
(∀𝑥∃*𝑦 𝑥𝑓𝑦 → ∀𝑥∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) |
43 | | relxp 5150 |
. . . . . . . . . 10
⊢ Rel
(𝐵 × 𝐴) |
44 | | relin2 5160 |
. . . . . . . . . 10
⊢ (Rel
(𝐵 × 𝐴) → Rel (𝑓 ∩ (𝐵 × 𝐴))) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . . 9
⊢ Rel
(𝑓 ∩ (𝐵 × 𝐴)) |
46 | | dffun6 5819 |
. . . . . . . . 9
⊢ (Fun
(𝑓 ∩ (𝐵 × 𝐴)) ↔ (Rel (𝑓 ∩ (𝐵 × 𝐴)) ∧ ∀𝑥∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
47 | 45, 46 | mpbiran 955 |
. . . . . . . 8
⊢ (Fun
(𝑓 ∩ (𝐵 × 𝐴)) ↔ ∀𝑥∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) |
48 | 42, 47 | sylibr 223 |
. . . . . . 7
⊢
(∀𝑥∃*𝑦 𝑥𝑓𝑦 → Fun (𝑓 ∩ (𝐵 × 𝐴))) |
49 | | funfn 5833 |
. . . . . . 7
⊢ (Fun
(𝑓 ∩ (𝐵 × 𝐴)) ↔ (𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴))) |
50 | 48, 49 | sylib 207 |
. . . . . 6
⊢
(∀𝑥∃*𝑦 𝑥𝑓𝑦 → (𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴))) |
51 | | rninxp 5492 |
. . . . . . 7
⊢ (ran
(𝑓 ∩ (𝐵 × 𝐴)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) |
52 | 51 | biimpri 217 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥 → ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴) |
53 | 50, 52 | anim12i 588 |
. . . . 5
⊢
((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → ((𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴)) |
54 | | df-fo 5810 |
. . . . 5
⊢ ((𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴 ↔ ((𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴)) |
55 | 53, 54 | sylibr 223 |
. . . 4
⊢
((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → (𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴) |
56 | | vex 3176 |
. . . . . . 7
⊢ 𝑓 ∈ V |
57 | 56 | inex1 4727 |
. . . . . 6
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ∈ V |
58 | 57 | dmex 6991 |
. . . . 5
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ∈ V |
59 | 58 | fodom 9227 |
. . . 4
⊢ ((𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴 → 𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴))) |
60 | | brdom3.2 |
. . . . . 6
⊢ 𝐵 ∈ V |
61 | | inss2 3796 |
. . . . . . . 8
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ⊆ (𝐵 × 𝐴) |
62 | | dmss 5245 |
. . . . . . . 8
⊢ ((𝑓 ∩ (𝐵 × 𝐴)) ⊆ (𝐵 × 𝐴) → dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ dom (𝐵 × 𝐴)) |
63 | 61, 62 | ax-mp 5 |
. . . . . . 7
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ dom (𝐵 × 𝐴) |
64 | | dmxpss 5484 |
. . . . . . 7
⊢ dom
(𝐵 × 𝐴) ⊆ 𝐵 |
65 | 63, 64 | sstri 3577 |
. . . . . 6
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐵 |
66 | | ssdomg 7887 |
. . . . . 6
⊢ (𝐵 ∈ V → (dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐵 → dom (𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵)) |
67 | 60, 65, 66 | mp2 9 |
. . . . 5
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵 |
68 | | domtr 7895 |
. . . . 5
⊢ ((𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ dom (𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵) → 𝐴 ≼ 𝐵) |
69 | 67, 68 | mpan2 703 |
. . . 4
⊢ (𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴)) → 𝐴 ≼ 𝐵) |
70 | 55, 59, 69 | 3syl 18 |
. . 3
⊢
((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ 𝐵) |
71 | 70 | exlimiv 1845 |
. 2
⊢
(∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ 𝐵) |
72 | 38, 71 | impbii 198 |
1
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |