| Step | Hyp | Ref
| Expression |
| 1 | | fofn 6822 |
. . . 4
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴) |
| 2 | 1 | 3ad2ant3 1136 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐹 Fn 𝐴) |
| 3 | | forn 6823 |
. . . . 5
⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) |
| 4 | | eqimss2 4043 |
. . . . 5
⊢ (ran
𝐹 = 𝐵 → 𝐵 ⊆ ran 𝐹) |
| 5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝐹:𝐴–onto→𝐵 → 𝐵 ⊆ ran 𝐹) |
| 6 | 5 | 3ad2ant3 1136 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ⊆ ran 𝐹) |
| 7 | | simp2 1138 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ Fin) |
| 8 | | fipreima 9398 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹 ∧ 𝐵 ∈ Fin) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)(𝐹 “ 𝑥) = 𝐵) |
| 9 | 2, 6, 7, 8 | syl3anc 1373 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)(𝐹 “ 𝑥) = 𝐵) |
| 10 | | elinel2 4202 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ Fin) |
| 11 | 10 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ Fin) |
| 12 | | finnum 9988 |
. . . . . . 7
⊢ (𝑥 ∈ Fin → 𝑥 ∈ dom
card) |
| 13 | 11, 12 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ dom card) |
| 14 | | simpl3 1194 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐴–onto→𝐵) |
| 15 | | fofun 6821 |
. . . . . . . 8
⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹) |
| 16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → Fun 𝐹) |
| 17 | | elinel1 4201 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴) |
| 18 | 17 | elpwid 4609 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ⊆ 𝐴) |
| 19 | 18 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ⊆ 𝐴) |
| 20 | | fof 6820 |
. . . . . . . . 9
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) |
| 21 | | fdm 6745 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
| 22 | 14, 20, 21 | 3syl 18 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → dom 𝐹 = 𝐴) |
| 23 | 19, 22 | sseqtrrd 4021 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ⊆ dom 𝐹) |
| 24 | | fores 6830 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑥 ⊆ dom 𝐹) → (𝐹 ↾ 𝑥):𝑥–onto→(𝐹 “ 𝑥)) |
| 25 | 16, 23, 24 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–onto→(𝐹 “ 𝑥)) |
| 26 | | fodomnum 10097 |
. . . . . 6
⊢ (𝑥 ∈ dom card → ((𝐹 ↾ 𝑥):𝑥–onto→(𝐹 “ 𝑥) → (𝐹 “ 𝑥) ≼ 𝑥)) |
| 27 | 13, 25, 26 | sylc 65 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ 𝑥) ≼ 𝑥) |
| 28 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐴 ∈ 𝑉) |
| 29 | | ssdomg 9040 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝑥 ⊆ 𝐴 → 𝑥 ≼ 𝐴)) |
| 30 | 28, 19, 29 | sylc 65 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ≼ 𝐴) |
| 31 | | domtr 9047 |
. . . . 5
⊢ (((𝐹 “ 𝑥) ≼ 𝑥 ∧ 𝑥 ≼ 𝐴) → (𝐹 “ 𝑥) ≼ 𝐴) |
| 32 | 27, 30, 31 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ 𝑥) ≼ 𝐴) |
| 33 | | breq1 5146 |
. . . 4
⊢ ((𝐹 “ 𝑥) = 𝐵 → ((𝐹 “ 𝑥) ≼ 𝐴 ↔ 𝐵 ≼ 𝐴)) |
| 34 | 32, 33 | syl5ibcom 245 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 “ 𝑥) = 𝐵 → 𝐵 ≼ 𝐴)) |
| 35 | 34 | rexlimdva 3155 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → (∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)(𝐹 “ 𝑥) = 𝐵 → 𝐵 ≼ 𝐴)) |
| 36 | 9, 35 | mpd 15 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴) |