Proof of Theorem brdom3
Step | Hyp | Ref
| Expression |
1 | | reldom 7961 |
. . . . . . . . 9
⊢ Rel
≼ |
2 | 1 | brrelexi 5158 |
. . . . . . . 8
⊢ (𝐴 ≼ 𝐵 → 𝐴 ∈ V) |
3 | | 0sdomg 8089 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝐴 ≼ 𝐵 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
5 | | df-ne 2795 |
. . . . . . 7
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) |
6 | 4, 5 | syl6bb 276 |
. . . . . 6
⊢ (𝐴 ≼ 𝐵 → (∅ ≺ 𝐴 ↔ ¬ 𝐴 = ∅)) |
7 | 6 | biimpar 502 |
. . . . 5
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 = ∅) → ∅ ≺ 𝐴) |
8 | | fodomr 8111 |
. . . . . 6
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ 𝐵) → ∃𝑓 𝑓:𝐵–onto→𝐴) |
9 | 8 | ancoms 469 |
. . . . 5
⊢ ((𝐴 ≼ 𝐵 ∧ ∅ ≺ 𝐴) → ∃𝑓 𝑓:𝐵–onto→𝐴) |
10 | 7, 9 | syldan 487 |
. . . 4
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 = ∅) → ∃𝑓 𝑓:𝐵–onto→𝐴) |
11 | | pm5.6 951 |
. . . 4
⊢ (((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 = ∅) → ∃𝑓 𝑓:𝐵–onto→𝐴) ↔ (𝐴 ≼ 𝐵 → (𝐴 = ∅ ∨ ∃𝑓 𝑓:𝐵–onto→𝐴))) |
12 | 10, 11 | mpbi 220 |
. . 3
⊢ (𝐴 ≼ 𝐵 → (𝐴 = ∅ ∨ ∃𝑓 𝑓:𝐵–onto→𝐴)) |
13 | | br0 4701 |
. . . . . . . 8
⊢ ¬
𝑥∅𝑦 |
14 | 13 | nex 1731 |
. . . . . . 7
⊢ ¬
∃𝑦 𝑥∅𝑦 |
15 | | exmo 2495 |
. . . . . . 7
⊢
(∃𝑦 𝑥∅𝑦 ∨ ∃*𝑦 𝑥∅𝑦) |
16 | 14, 15 | mtpor 1695 |
. . . . . 6
⊢
∃*𝑦 𝑥∅𝑦 |
17 | 16 | ax-gen 1722 |
. . . . 5
⊢
∀𝑥∃*𝑦 𝑥∅𝑦 |
18 | | rzal 4073 |
. . . . 5
⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦∅𝑥) |
19 | | 0ex 4790 |
. . . . . 6
⊢ ∅
∈ V |
20 | | breq 4655 |
. . . . . . . . 9
⊢ (𝑓 = ∅ → (𝑥𝑓𝑦 ↔ 𝑥∅𝑦)) |
21 | 20 | mobidv 2491 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (∃*𝑦 𝑥𝑓𝑦 ↔ ∃*𝑦 𝑥∅𝑦)) |
22 | 21 | albidv 1849 |
. . . . . . 7
⊢ (𝑓 = ∅ → (∀𝑥∃*𝑦 𝑥𝑓𝑦 ↔ ∀𝑥∃*𝑦 𝑥∅𝑦)) |
23 | | breq 4655 |
. . . . . . . . 9
⊢ (𝑓 = ∅ → (𝑦𝑓𝑥 ↔ 𝑦∅𝑥)) |
24 | 23 | rexbidv 3052 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (∃𝑦 ∈ 𝐵 𝑦𝑓𝑥 ↔ ∃𝑦 ∈ 𝐵 𝑦∅𝑥)) |
25 | 24 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑓 = ∅ → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦∅𝑥)) |
26 | 22, 25 | anbi12d 747 |
. . . . . 6
⊢ (𝑓 = ∅ →
((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) ↔ (∀𝑥∃*𝑦 𝑥∅𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦∅𝑥))) |
27 | 19, 26 | spcev 3300 |
. . . . 5
⊢
((∀𝑥∃*𝑦 𝑥∅𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦∅𝑥) → ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
28 | 17, 18, 27 | sylancr 695 |
. . . 4
⊢ (𝐴 = ∅ → ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
29 | | fofun 6116 |
. . . . . . 7
⊢ (𝑓:𝐵–onto→𝐴 → Fun 𝑓) |
30 | | dffun6 5903 |
. . . . . . . 8
⊢ (Fun
𝑓 ↔ (Rel 𝑓 ∧ ∀𝑥∃*𝑦 𝑥𝑓𝑦)) |
31 | 30 | simprbi 480 |
. . . . . . 7
⊢ (Fun
𝑓 → ∀𝑥∃*𝑦 𝑥𝑓𝑦) |
32 | 29, 31 | syl 17 |
. . . . . 6
⊢ (𝑓:𝐵–onto→𝐴 → ∀𝑥∃*𝑦 𝑥𝑓𝑦) |
33 | | dffo4 6375 |
. . . . . . 7
⊢ (𝑓:𝐵–onto→𝐴 ↔ (𝑓:𝐵⟶𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
34 | 33 | simprbi 480 |
. . . . . 6
⊢ (𝑓:𝐵–onto→𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) |
35 | 32, 34 | jca 554 |
. . . . 5
⊢ (𝑓:𝐵–onto→𝐴 → (∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
36 | 35 | eximi 1762 |
. . . 4
⊢
(∃𝑓 𝑓:𝐵–onto→𝐴 → ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
37 | 28, 36 | jaoi 394 |
. . 3
⊢ ((𝐴 = ∅ ∨ ∃𝑓 𝑓:𝐵–onto→𝐴) → ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
38 | 12, 37 | syl 17 |
. 2
⊢ (𝐴 ≼ 𝐵 → ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
39 | | inss1 3833 |
. . . . . . . . . . 11
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝑓 |
40 | 39 | ssbri 4697 |
. . . . . . . . . 10
⊢ (𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦 → 𝑥𝑓𝑦) |
41 | 40 | moimi 2520 |
. . . . . . . . 9
⊢
(∃*𝑦 𝑥𝑓𝑦 → ∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) |
42 | 41 | alimi 1739 |
. . . . . . . 8
⊢
(∀𝑥∃*𝑦 𝑥𝑓𝑦 → ∀𝑥∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) |
43 | | relxp 5227 |
. . . . . . . . . 10
⊢ Rel
(𝐵 × 𝐴) |
44 | | relin2 5237 |
. . . . . . . . . 10
⊢ (Rel
(𝐵 × 𝐴) → Rel (𝑓 ∩ (𝐵 × 𝐴))) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . . 9
⊢ Rel
(𝑓 ∩ (𝐵 × 𝐴)) |
46 | | dffun6 5903 |
. . . . . . . . 9
⊢ (Fun
(𝑓 ∩ (𝐵 × 𝐴)) ↔ (Rel (𝑓 ∩ (𝐵 × 𝐴)) ∧ ∀𝑥∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
47 | 45, 46 | mpbiran 953 |
. . . . . . . 8
⊢ (Fun
(𝑓 ∩ (𝐵 × 𝐴)) ↔ ∀𝑥∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) |
48 | 42, 47 | sylibr 224 |
. . . . . . 7
⊢
(∀𝑥∃*𝑦 𝑥𝑓𝑦 → Fun (𝑓 ∩ (𝐵 × 𝐴))) |
49 | | funfn 5918 |
. . . . . . 7
⊢ (Fun
(𝑓 ∩ (𝐵 × 𝐴)) ↔ (𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴))) |
50 | 48, 49 | sylib 208 |
. . . . . 6
⊢
(∀𝑥∃*𝑦 𝑥𝑓𝑦 → (𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴))) |
51 | | rninxp 5573 |
. . . . . . 7
⊢ (ran
(𝑓 ∩ (𝐵 × 𝐴)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) |
52 | 51 | biimpri 218 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥 → ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴) |
53 | 50, 52 | anim12i 590 |
. . . . 5
⊢
((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → ((𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴)) |
54 | | df-fo 5894 |
. . . . 5
⊢ ((𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴 ↔ ((𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴)) |
55 | 53, 54 | sylibr 224 |
. . . 4
⊢
((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → (𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴) |
56 | | vex 3203 |
. . . . . . 7
⊢ 𝑓 ∈ V |
57 | 56 | inex1 4799 |
. . . . . 6
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ∈ V |
58 | 57 | dmex 7099 |
. . . . 5
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ∈ V |
59 | 58 | fodom 9344 |
. . . 4
⊢ ((𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴 → 𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴))) |
60 | | brdom3.2 |
. . . . . 6
⊢ 𝐵 ∈ V |
61 | | inss2 3834 |
. . . . . . . 8
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ⊆ (𝐵 × 𝐴) |
62 | | dmss 5323 |
. . . . . . . 8
⊢ ((𝑓 ∩ (𝐵 × 𝐴)) ⊆ (𝐵 × 𝐴) → dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ dom (𝐵 × 𝐴)) |
63 | 61, 62 | ax-mp 5 |
. . . . . . 7
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ dom (𝐵 × 𝐴) |
64 | | dmxpss 5565 |
. . . . . . 7
⊢ dom
(𝐵 × 𝐴) ⊆ 𝐵 |
65 | 63, 64 | sstri 3612 |
. . . . . 6
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐵 |
66 | | ssdomg 8001 |
. . . . . 6
⊢ (𝐵 ∈ V → (dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐵 → dom (𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵)) |
67 | 60, 65, 66 | mp2 9 |
. . . . 5
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵 |
68 | | domtr 8009 |
. . . . 5
⊢ ((𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ dom (𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵) → 𝐴 ≼ 𝐵) |
69 | 67, 68 | mpan2 707 |
. . . 4
⊢ (𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴)) → 𝐴 ≼ 𝐵) |
70 | 55, 59, 69 | 3syl 18 |
. . 3
⊢
((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ 𝐵) |
71 | 70 | exlimiv 1858 |
. 2
⊢
(∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ 𝐵) |
72 | 38, 71 | impbii 199 |
1
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |