Proof of Theorem brdom4
| Step | Hyp | Ref
| Expression |
| 1 | | brdom3.2 |
. . . 4
⊢ 𝐵 ∈ V |
| 2 | 1 | brdom3 10568 |
. . 3
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
| 3 | | mormo 3385 |
. . . . . . 7
⊢
(∃*𝑦 𝑥𝑓𝑦 → ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦) |
| 4 | 3 | alimi 1811 |
. . . . . 6
⊢
(∀𝑥∃*𝑦 𝑥𝑓𝑦 → ∀𝑥∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦) |
| 5 | | alral 3075 |
. . . . . 6
⊢
(∀𝑥∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 → ∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦) |
| 6 | 4, 5 | syl 17 |
. . . . 5
⊢
(∀𝑥∃*𝑦 𝑥𝑓𝑦 → ∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦) |
| 7 | 6 | anim1i 615 |
. . . 4
⊢
((∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → (∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
| 8 | 7 | eximi 1835 |
. . 3
⊢
(∃𝑓(∀𝑥∃*𝑦 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
| 9 | 2, 8 | sylbi 217 |
. 2
⊢ (𝐴 ≼ 𝐵 → ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |
| 10 | | inss2 4238 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ⊆ (𝐵 × 𝐴) |
| 11 | | dmss 5913 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∩ (𝐵 × 𝐴)) ⊆ (𝐵 × 𝐴) → dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ dom (𝐵 × 𝐴)) |
| 12 | 10, 11 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ dom (𝐵 × 𝐴) |
| 13 | | dmxpss 6191 |
. . . . . . . . . . . . . 14
⊢ dom
(𝐵 × 𝐴) ⊆ 𝐵 |
| 14 | 12, 13 | sstri 3993 |
. . . . . . . . . . . . 13
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐵 |
| 15 | 14 | sseli 3979 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴)) → 𝑥 ∈ 𝐵) |
| 16 | 10 | rnssi 5951 |
. . . . . . . . . . . . . . . . 17
⊢ ran
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ ran (𝐵 × 𝐴) |
| 17 | | rnxpss 6192 |
. . . . . . . . . . . . . . . . 17
⊢ ran
(𝐵 × 𝐴) ⊆ 𝐴 |
| 18 | 16, 17 | sstri 3993 |
. . . . . . . . . . . . . . . 16
⊢ ran
(𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐴 |
| 19 | 18 | sseli 3979 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴)) → 𝑦 ∈ 𝐴) |
| 20 | | inss1 4237 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝑓 |
| 21 | 20 | ssbri 5188 |
. . . . . . . . . . . . . . 15
⊢ (𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦 → 𝑥𝑓𝑦) |
| 22 | 19, 21 | anim12i 613 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴)) ∧ 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) → (𝑦 ∈ 𝐴 ∧ 𝑥𝑓𝑦)) |
| 23 | 22 | moimi 2545 |
. . . . . . . . . . . . 13
⊢
(∃*𝑦(𝑦 ∈ 𝐴 ∧ 𝑥𝑓𝑦) → ∃*𝑦(𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴)) ∧ 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
| 24 | | df-rmo 3380 |
. . . . . . . . . . . . 13
⊢
(∃*𝑦 ∈
𝐴 𝑥𝑓𝑦 ↔ ∃*𝑦(𝑦 ∈ 𝐴 ∧ 𝑥𝑓𝑦)) |
| 25 | | df-rmo 3380 |
. . . . . . . . . . . . 13
⊢
(∃*𝑦 ∈
ran (𝑓 ∩ (𝐵 × 𝐴))𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦 ↔ ∃*𝑦(𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴)) ∧ 𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
| 26 | 23, 24, 25 | 3imtr4i 292 |
. . . . . . . . . . . 12
⊢
(∃*𝑦 ∈
𝐴 𝑥𝑓𝑦 → ∃*𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴))𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) |
| 27 | 15, 26 | imim12i 62 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐵 → ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦) → (𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴)) → ∃*𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴))𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
| 28 | 27 | ralimi2 3078 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 → ∀𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴))∃*𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴))𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦) |
| 29 | | relinxp 5824 |
. . . . . . . . . 10
⊢ Rel
(𝑓 ∩ (𝐵 × 𝐴)) |
| 30 | 28, 29 | jctil 519 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 → (Rel (𝑓 ∩ (𝐵 × 𝐴)) ∧ ∀𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴))∃*𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴))𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
| 31 | | dffun9 6595 |
. . . . . . . . 9
⊢ (Fun
(𝑓 ∩ (𝐵 × 𝐴)) ↔ (Rel (𝑓 ∩ (𝐵 × 𝐴)) ∧ ∀𝑥 ∈ dom (𝑓 ∩ (𝐵 × 𝐴))∃*𝑦 ∈ ran (𝑓 ∩ (𝐵 × 𝐴))𝑥(𝑓 ∩ (𝐵 × 𝐴))𝑦)) |
| 32 | 30, 31 | sylibr 234 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 → Fun (𝑓 ∩ (𝐵 × 𝐴))) |
| 33 | 32 | funfnd 6597 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 → (𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴))) |
| 34 | | rninxp 6199 |
. . . . . . . 8
⊢ (ran
(𝑓 ∩ (𝐵 × 𝐴)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) |
| 35 | 34 | biimpri 228 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥 → ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴) |
| 36 | 33, 35 | anim12i 613 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → ((𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴)) |
| 37 | | df-fo 6567 |
. . . . . 6
⊢ ((𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴 ↔ ((𝑓 ∩ (𝐵 × 𝐴)) Fn dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ ran (𝑓 ∩ (𝐵 × 𝐴)) = 𝐴)) |
| 38 | 36, 37 | sylibr 234 |
. . . . 5
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → (𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴) |
| 39 | | vex 3484 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
| 40 | 39 | inex1 5317 |
. . . . . . 7
⊢ (𝑓 ∩ (𝐵 × 𝐴)) ∈ V |
| 41 | 40 | dmex 7931 |
. . . . . 6
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ∈ V |
| 42 | 41 | fodom 10563 |
. . . . 5
⊢ ((𝑓 ∩ (𝐵 × 𝐴)):dom (𝑓 ∩ (𝐵 × 𝐴))–onto→𝐴 → 𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴))) |
| 43 | 38, 42 | syl 17 |
. . . 4
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴))) |
| 44 | | ssdomg 9040 |
. . . . 5
⊢ (𝐵 ∈ V → (dom (𝑓 ∩ (𝐵 × 𝐴)) ⊆ 𝐵 → dom (𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵)) |
| 45 | 1, 14, 44 | mp2 9 |
. . . 4
⊢ dom
(𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵 |
| 46 | | domtr 9047 |
. . . 4
⊢ ((𝐴 ≼ dom (𝑓 ∩ (𝐵 × 𝐴)) ∧ dom (𝑓 ∩ (𝐵 × 𝐴)) ≼ 𝐵) → 𝐴 ≼ 𝐵) |
| 47 | 43, 45, 46 | sylancl 586 |
. . 3
⊢
((∀𝑥 ∈
𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ 𝐵) |
| 48 | 47 | exlimiv 1930 |
. 2
⊢
(∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥) → 𝐴 ≼ 𝐵) |
| 49 | 9, 48 | impbii 209 |
1
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓(∀𝑥 ∈ 𝐵 ∃*𝑦 ∈ 𝐴 𝑥𝑓𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑦𝑓𝑥)) |