Proof of Theorem brdom5
Step | Hyp | Ref
| Expression |
1 | | brdom3.2 |
. . . 4
⊢ 𝐵 ∈ V |
2 | 1 | brdom3 9350 |
. . 3
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
3 | | alral 2928 |
. . . . 5
⊢
(∀𝑥∃*𝑦 𝑥𝑓𝑦 → ∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦) |
4 | 3 | anim1i 592 |
. . . 4
⊢
((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → (∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
5 | 4 | eximi 1762 |
. . 3
⊢
(∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
6 | 2, 5 | sylbi 207 |
. 2
⊢ (𝐴 ≼ 𝐵 → ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
7 | | inss2 3834 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ⊆ (𝐵 × 𝐴) |
8 | | dmss 5323 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∩ (𝐵 × 𝐴)) ⊆ (𝐵 × 𝐴) → dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ dom (𝐵 × 𝐴)) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ dom (𝐵 × 𝐴) |
10 | | dmxpss 5565 |
. . . . . . . . . . . . 13
⊢ dom
(𝐵 × 𝐴) ⊆ 𝐵 |
11 | 9, 10 | sstri 3612 |
. . . . . . . . . . . 12
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐵 |
12 | 11 | sseli 3599 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴)) → 𝑥 ∈ 𝐵) |
13 | | inss1 3833 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝑓 |
14 | 13 | ssbri 4697 |
. . . . . . . . . . . 12
⊢ (𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦 → 𝑥𝑓𝑦) |
15 | 14 | moimi 2520 |
. . . . . . . . . . 11
⊢
(∃*𝑦 𝑥𝑓𝑦 → ∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) |
16 | 12, 15 | imim12i 62 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 → ∃*𝑦 𝑥𝑓𝑦) → (𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴)) → ∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
17 | 16 | ralimi2 2949 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 𝑥𝑓𝑦 → ∀𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴))∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) |
18 | | relxp 5227 |
. . . . . . . . . 10
⊢ Rel
(𝐵 × 𝐴) |
19 | | relin2 5237 |
. . . . . . . . . 10
⊢ (Rel
(𝐵 × 𝐴) → Rel (𝑓 ∩ (𝐵 × 𝐴))) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . 9
⊢ Rel
(𝑓 ∩ (𝐵 × 𝐴)) |
21 | 17, 20 | jctil 560 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 𝑥𝑓𝑦 → (Rel (𝑓 ∩ (𝐵 × 𝐴)) ∧ ∀𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴))∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
22 | | dffun7 5915 |
. . . . . . . 8
⊢ (Fun
(𝑓 ∩ (𝐵 × 𝐴)) ↔ (Rel (𝑓 ∩ (𝐵 × 𝐴)) ∧ ∀𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴))∃*𝑦 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
23 | 21, 22 | sylibr 224 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 𝑥𝑓𝑦 → Fun (𝑓 ∩ (𝐵 × 𝐴))) |
24 | | funfn 5918 |
. . . . . . 7
⊢ (Fun
(𝑓 ∩ (𝐵 × 𝐴)) ↔ (𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴))) |
25 | 23, 24 | sylib 208 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 𝑥𝑓𝑦 → (𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴))) |
26 | | rninxp 5573 |
. . . . . . 7
⊢ (ran
(𝑓 ∩ (𝐵 × 𝐴)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) |
27 | 26 | biimpri 218 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥 → ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴) |
28 | 25, 27 | anim12i 590 |
. . . . 5
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → ((𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴)) |
29 | | df-fo 5894 |
. . . . 5
⊢ ((𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴 ↔ ((𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴)) |
30 | 28, 29 | sylibr 224 |
. . . 4
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → (𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴) |
31 | | vex 3203 |
. . . . . . 7
⊢ 𝑓 ∈ V |
32 | 31 | inex1 4799 |
. . . . . 6
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ∈ V |
33 | 32 | dmex 7099 |
. . . . 5
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ∈ V |
34 | 33 | fodom 9344 |
. . . 4
⊢ ((𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴 → 𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴))) |
35 | | ssdomg 8001 |
. . . . . 6
⊢ (𝐵 ∈ V → (dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐵 → dom (𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵)) |
36 | 1, 11, 35 | mp2 9 |
. . . . 5
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵 |
37 | | domtr 8009 |
. . . . 5
⊢ ((𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ dom (𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵) → 𝐴 ≼ 𝐵) |
38 | 36, 37 | mpan2 707 |
. . . 4
⊢ (𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴)) → 𝐴 ≼ 𝐵) |
39 | 30, 34, 38 | 3syl 18 |
. . 3
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ 𝐵) |
40 | 39 | exlimiv 1858 |
. 2
⊢
(∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ 𝐵) |
41 | 6, 40 | impbii 199 |
1
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |