Proof of Theorem brdom4
Step | Hyp | Ref
| Expression |
1 | | brdom3.2 |
. . . 4
⊢ 𝐵 ∈ V |
2 | 1 | brdom3 9231 |
. . 3
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
3 | | mormo 3135 |
. . . . . . 7
⊢
(∃*𝑦 𝑥𝑓𝑦 → ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦) |
4 | 3 | alimi 1730 |
. . . . . 6
⊢
(∀𝑥∃*𝑦 𝑥𝑓𝑦 → ∀𝑥∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦) |
5 | | alral 2912 |
. . . . . 6
⊢
(∀𝑥∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 → ∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢
(∀𝑥∃*𝑦 𝑥𝑓𝑦 → ∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦) |
7 | 6 | anim1i 590 |
. . . 4
⊢
((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → (∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
8 | 7 | eximi 1752 |
. . 3
⊢
(∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
9 | 2, 8 | sylbi 206 |
. 2
⊢ (𝐴 ≼ 𝐵 → ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
10 | | inss2 3796 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ⊆ (𝐵 × 𝐴) |
11 | | dmss 5245 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∩ (𝐵 × 𝐴)) ⊆ (𝐵 × 𝐴) → dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ dom (𝐵 × 𝐴)) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ dom (𝐵 × 𝐴) |
13 | | dmxpss 5484 |
. . . . . . . . . . . . . 14
⊢ dom
(𝐵 × 𝐴) ⊆ 𝐵 |
14 | 12, 13 | sstri 3577 |
. . . . . . . . . . . . 13
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐵 |
15 | 14 | sseli 3564 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴)) → 𝑥 ∈ 𝐵) |
16 | | rnss 5275 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∩ (𝐵 × 𝐴)) ⊆ (𝐵 × 𝐴) → ran (𝑓 ∩ (𝐵 × 𝐴)) ⊆ ran (𝐵 × 𝐴)) |
17 | 10, 16 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ran
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ ran (𝐵 × 𝐴) |
18 | | rnxpss 5485 |
. . . . . . . . . . . . . . . . 17
⊢ ran
(𝐵 × 𝐴) ⊆ 𝐴 |
19 | 17, 18 | sstri 3577 |
. . . . . . . . . . . . . . . 16
⊢ ran
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐴 |
20 | 19 | sseli 3564 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴)) → 𝑦 ∈ 𝐴) |
21 | | inss1 3795 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝑓 |
22 | 21 | ssbri 4627 |
. . . . . . . . . . . . . . 15
⊢ (𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦 → 𝑥𝑓𝑦) |
23 | 20, 22 | anim12i 588 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴)) ∧ 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) → (𝑦 ∈ 𝐴 ∧ 𝑥𝑓𝑦)) |
24 | 23 | moimi 2508 |
. . . . . . . . . . . . 13
⊢
(∃*𝑦(𝑦 ∈ 𝐴 ∧ 𝑥𝑓𝑦) → ∃*𝑦(𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴)) ∧ 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
25 | | df-rmo 2904 |
. . . . . . . . . . . . 13
⊢
(∃*𝑦 ∈
𝐴 𝑥𝑓𝑦 ↔ ∃*𝑦(𝑦 ∈ 𝐴 ∧ 𝑥𝑓𝑦)) |
26 | | df-rmo 2904 |
. . . . . . . . . . . . 13
⊢
(∃*𝑦 ∈
ran (𝑓 ∩ (𝐵 × 𝐴))𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦 ↔ ∃*𝑦(𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴)) ∧ 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
27 | 24, 25, 26 | 3imtr4i 280 |
. . . . . . . . . . . 12
⊢
(∃*𝑦 ∈
𝐴 𝑥𝑓𝑦 → ∃*𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴))𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) |
28 | 15, 27 | imim12i 60 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐵 → ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦) → (𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴)) → ∃*𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴))𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
29 | 28 | ralimi2 2933 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 → ∀𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴))∃*𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴))𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) |
30 | | relxp 5150 |
. . . . . . . . . . 11
⊢ Rel
(𝐵 × 𝐴) |
31 | | relin2 5160 |
. . . . . . . . . . 11
⊢ (Rel
(𝐵 × 𝐴) → Rel (𝑓 ∩ (𝐵 × 𝐴))) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . 10
⊢ Rel
(𝑓 ∩ (𝐵 × 𝐴)) |
33 | 29, 32 | jctil 558 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 → (Rel (𝑓 ∩ (𝐵 × 𝐴)) ∧ ∀𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴))∃*𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴))𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
34 | | dffun9 5832 |
. . . . . . . . 9
⊢ (Fun
(𝑓 ∩ (𝐵 × 𝐴)) ↔ (Rel (𝑓 ∩ (𝐵 × 𝐴)) ∧ ∀𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴))∃*𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴))𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
35 | 33, 34 | sylibr 223 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 → Fun (𝑓 ∩ (𝐵 × 𝐴))) |
36 | | funfn 5833 |
. . . . . . . 8
⊢ (Fun
(𝑓 ∩ (𝐵 × 𝐴)) ↔ (𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴))) |
37 | 35, 36 | sylib 207 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 → (𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴))) |
38 | | rninxp 5492 |
. . . . . . . 8
⊢ (ran
(𝑓 ∩ (𝐵 × 𝐴)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) |
39 | 38 | biimpri 217 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥 → ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴) |
40 | 37, 39 | anim12i 588 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → ((𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴)) |
41 | | df-fo 5810 |
. . . . . 6
⊢ ((𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴 ↔ ((𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴)) |
42 | 40, 41 | sylibr 223 |
. . . . 5
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → (𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴) |
43 | | vex 3176 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
44 | 43 | inex1 4727 |
. . . . . . 7
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ∈ V |
45 | 44 | dmex 6991 |
. . . . . 6
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ∈ V |
46 | 45 | fodom 9227 |
. . . . 5
⊢ ((𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴 → 𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴))) |
47 | 42, 46 | syl 17 |
. . . 4
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴))) |
48 | | ssdomg 7887 |
. . . . 5
⊢ (𝐵 ∈ V → (dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐵 → dom (𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵)) |
49 | 1, 14, 48 | mp2 9 |
. . . 4
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵 |
50 | | domtr 7895 |
. . . 4
⊢ ((𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ dom (𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵) → 𝐴 ≼ 𝐵) |
51 | 47, 49, 50 | sylancl 693 |
. . 3
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ 𝐵) |
52 | 51 | exlimiv 1845 |
. 2
⊢
(∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ 𝐵) |
53 | 9, 52 | impbii 198 |
1
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |