Step | Hyp | Ref
| Expression |
1 | | fofn 6030 |
. . . 4
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴) |
2 | 1 | 3ad2ant3 1077 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐹 Fn 𝐴) |
3 | | forn 6031 |
. . . . 5
⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵) |
4 | | eqimss2 3621 |
. . . . 5
⊢ (ran
𝐹 = 𝐵 → 𝐵 ⊆ ran 𝐹) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝐹:𝐴–onto→𝐵 → 𝐵 ⊆ ran 𝐹) |
6 | 5 | 3ad2ant3 1077 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ⊆ ran 𝐹) |
7 | | simp2 1055 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ Fin) |
8 | | fipreima 8155 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹 ∧ 𝐵 ∈ Fin) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)(𝐹 “ 𝑥) = 𝐵) |
9 | 2, 6, 7, 8 | syl3anc 1318 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)(𝐹 “ 𝑥) = 𝐵) |
10 | | inss2 3796 |
. . . . . . . . 9
⊢
(𝒫 𝐴 ∩
Fin) ⊆ Fin |
11 | 10 | sseli 3564 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ Fin) |
12 | 11 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ Fin) |
13 | | finnum 8657 |
. . . . . . 7
⊢ (𝑥 ∈ Fin → 𝑥 ∈ dom
card) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ dom card) |
15 | | simpl3 1059 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐴–onto→𝐵) |
16 | | fofun 6029 |
. . . . . . . 8
⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹) |
17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → Fun 𝐹) |
18 | | inss1 3795 |
. . . . . . . . . . 11
⊢
(𝒫 𝐴 ∩
Fin) ⊆ 𝒫 𝐴 |
19 | 18 | sseli 3564 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴) |
20 | 19 | elpwid 4118 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ⊆ 𝐴) |
21 | 20 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ⊆ 𝐴) |
22 | | fof 6028 |
. . . . . . . . 9
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵) |
23 | | fdm 5964 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
24 | 15, 22, 23 | 3syl 18 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → dom 𝐹 = 𝐴) |
25 | 21, 24 | sseqtr4d 3605 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ⊆ dom 𝐹) |
26 | | fores 6037 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑥 ⊆ dom 𝐹) → (𝐹 ↾ 𝑥):𝑥–onto→(𝐹 “ 𝑥)) |
27 | 17, 25, 26 | syl2anc 691 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–onto→(𝐹 “ 𝑥)) |
28 | | fodomnum 8763 |
. . . . . 6
⊢ (𝑥 ∈ dom card → ((𝐹 ↾ 𝑥):𝑥–onto→(𝐹 “ 𝑥) → (𝐹 “ 𝑥) ≼ 𝑥)) |
29 | 14, 27, 28 | sylc 63 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ 𝑥) ≼ 𝑥) |
30 | | simpl1 1057 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐴 ∈ 𝑉) |
31 | | ssdomg 7887 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝑥 ⊆ 𝐴 → 𝑥 ≼ 𝐴)) |
32 | 30, 21, 31 | sylc 63 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ≼ 𝐴) |
33 | | domtr 7895 |
. . . . 5
⊢ (((𝐹 “ 𝑥) ≼ 𝑥 ∧ 𝑥 ≼ 𝐴) → (𝐹 “ 𝑥) ≼ 𝐴) |
34 | 29, 32, 33 | syl2anc 691 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ 𝑥) ≼ 𝐴) |
35 | | breq1 4586 |
. . . 4
⊢ ((𝐹 “ 𝑥) = 𝐵 → ((𝐹 “ 𝑥) ≼ 𝐴 ↔ 𝐵 ≼ 𝐴)) |
36 | 34, 35 | syl5ibcom 234 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 “ 𝑥) = 𝐵 → 𝐵 ≼ 𝐴)) |
37 | 36 | rexlimdva 3013 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → (∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)(𝐹 “ 𝑥) = 𝐵 → 𝐵 ≼ 𝐴)) |
38 | 9, 37 | mpd 15 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴) |