Step | Hyp | Ref
| Expression |
1 | | foima 6839 |
. . 3
⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵) |
2 | 1 | adantl 481 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → (𝐹 “ 𝐴) = 𝐵) |
3 | | imaeq2 6085 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝐹 “ 𝑥) = (𝐹 “ ∅)) |
4 | | ima0 6106 |
. . . . . . 7
⊢ (𝐹 “ ∅) =
∅ |
5 | 3, 4 | eqtrdi 2796 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐹 “ 𝑥) = ∅) |
6 | | id 22 |
. . . . . 6
⊢ (𝑥 = ∅ → 𝑥 = ∅) |
7 | 5, 6 | breq12d 5179 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐹 “ 𝑥) ≼ 𝑥 ↔ ∅ ≼
∅)) |
8 | 7 | imbi2d 340 |
. . . 4
⊢ (𝑥 = ∅ → ((𝐹 Fn 𝐴 → (𝐹 “ 𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → ∅ ≼
∅))) |
9 | | imaeq2 6085 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐹 “ 𝑥) = (𝐹 “ 𝑦)) |
10 | | id 22 |
. . . . . 6
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
11 | 9, 10 | breq12d 5179 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐹 “ 𝑥) ≼ 𝑥 ↔ (𝐹 “ 𝑦) ≼ 𝑦)) |
12 | 11 | imbi2d 340 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐹 Fn 𝐴 → (𝐹 “ 𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹 “ 𝑦) ≼ 𝑦))) |
13 | | imaeq2 6085 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹 “ 𝑥) = (𝐹 “ (𝑦 ∪ {𝑧}))) |
14 | | id 22 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → 𝑥 = (𝑦 ∪ {𝑧})) |
15 | 13, 14 | breq12d 5179 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐹 “ 𝑥) ≼ 𝑥 ↔ (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧}))) |
16 | 15 | imbi2d 340 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐹 Fn 𝐴 → (𝐹 “ 𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧})))) |
17 | | imaeq2 6085 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝐹 “ 𝑥) = (𝐹 “ 𝐴)) |
18 | | id 22 |
. . . . . 6
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) |
19 | 17, 18 | breq12d 5179 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝐹 “ 𝑥) ≼ 𝑥 ↔ (𝐹 “ 𝐴) ≼ 𝐴)) |
20 | 19 | imbi2d 340 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝐹 Fn 𝐴 → (𝐹 “ 𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) ≼ 𝐴))) |
21 | | 0ex 5325 |
. . . . . 6
⊢ ∅
∈ V |
22 | 21 | 0dom 9172 |
. . . . 5
⊢ ∅
≼ ∅ |
23 | 22 | a1i 11 |
. . . 4
⊢ (𝐹 Fn 𝐴 → ∅ ≼
∅) |
24 | | fnfun 6679 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝐴 → Fun 𝐹) |
25 | 24 | ad2antrl 727 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → Fun 𝐹) |
26 | | funressn 7193 |
. . . . . . . . . . . . 13
⊢ (Fun
𝐹 → (𝐹 ↾ {𝑧}) ⊆ {〈𝑧, (𝐹‘𝑧)〉}) |
27 | | rnss 5964 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ↾ {𝑧}) ⊆ {〈𝑧, (𝐹‘𝑧)〉} → ran (𝐹 ↾ {𝑧}) ⊆ ran {〈𝑧, (𝐹‘𝑧)〉}) |
28 | 25, 26, 27 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ran (𝐹 ↾ {𝑧}) ⊆ ran {〈𝑧, (𝐹‘𝑧)〉}) |
29 | | df-ima 5713 |
. . . . . . . . . . . 12
⊢ (𝐹 “ {𝑧}) = ran (𝐹 ↾ {𝑧}) |
30 | | vex 3492 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
31 | 30 | rnsnop 6255 |
. . . . . . . . . . . . 13
⊢ ran
{〈𝑧, (𝐹‘𝑧)〉} = {(𝐹‘𝑧)} |
32 | 31 | eqcomi 2749 |
. . . . . . . . . . . 12
⊢ {(𝐹‘𝑧)} = ran {〈𝑧, (𝐹‘𝑧)〉} |
33 | 28, 29, 32 | 3sstr4g 4054 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ⊆ {(𝐹‘𝑧)}) |
34 | | snfi 9109 |
. . . . . . . . . . 11
⊢ {(𝐹‘𝑧)} ∈ Fin |
35 | | ssexg 5341 |
. . . . . . . . . . 11
⊢ (((𝐹 “ {𝑧}) ⊆ {(𝐹‘𝑧)} ∧ {(𝐹‘𝑧)} ∈ Fin) → (𝐹 “ {𝑧}) ∈ V) |
36 | 33, 34, 35 | sylancl 585 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ∈ V) |
37 | | fvi 6998 |
. . . . . . . . . 10
⊢ ((𝐹 “ {𝑧}) ∈ V → ( I ‘(𝐹 “ {𝑧})) = (𝐹 “ {𝑧})) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ( I ‘(𝐹 “ {𝑧})) = (𝐹 “ {𝑧})) |
39 | 38 | uneq2d 4191 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ((𝐹 “ 𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) = ((𝐹 “ 𝑦) ∪ (𝐹 “ {𝑧}))) |
40 | | imaundi 6181 |
. . . . . . . 8
⊢ (𝐹 “ (𝑦 ∪ {𝑧})) = ((𝐹 “ 𝑦) ∪ (𝐹 “ {𝑧})) |
41 | 39, 40 | eqtr4di 2798 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ((𝐹 “ 𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) = (𝐹 “ (𝑦 ∪ {𝑧}))) |
42 | | simprr 772 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ 𝑦) ≼ 𝑦) |
43 | | ssdomfi 9262 |
. . . . . . . . . . 11
⊢ ({(𝐹‘𝑧)} ∈ Fin → ((𝐹 “ {𝑧}) ⊆ {(𝐹‘𝑧)} → (𝐹 “ {𝑧}) ≼ {(𝐹‘𝑧)})) |
44 | 34, 33, 43 | mpsyl 68 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ≼ {(𝐹‘𝑧)}) |
45 | | fvex 6933 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑧) ∈ V |
46 | | en2sn 9106 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑧) ∈ V ∧ 𝑧 ∈ V) → {(𝐹‘𝑧)} ≈ {𝑧}) |
47 | 45, 30, 46 | mp2an 691 |
. . . . . . . . . 10
⊢ {(𝐹‘𝑧)} ≈ {𝑧} |
48 | | endom 9039 |
. . . . . . . . . . 11
⊢ ({(𝐹‘𝑧)} ≈ {𝑧} → {(𝐹‘𝑧)} ≼ {𝑧}) |
49 | | domtrfi 9259 |
. . . . . . . . . . . 12
⊢ (({(𝐹‘𝑧)} ∈ Fin ∧ (𝐹 “ {𝑧}) ≼ {(𝐹‘𝑧)} ∧ {(𝐹‘𝑧)} ≼ {𝑧}) → (𝐹 “ {𝑧}) ≼ {𝑧}) |
50 | 34, 49 | mp3an1 1448 |
. . . . . . . . . . 11
⊢ (((𝐹 “ {𝑧}) ≼ {(𝐹‘𝑧)} ∧ {(𝐹‘𝑧)} ≼ {𝑧}) → (𝐹 “ {𝑧}) ≼ {𝑧}) |
51 | 48, 50 | sylan2 592 |
. . . . . . . . . 10
⊢ (((𝐹 “ {𝑧}) ≼ {(𝐹‘𝑧)} ∧ {(𝐹‘𝑧)} ≈ {𝑧}) → (𝐹 “ {𝑧}) ≼ {𝑧}) |
52 | 44, 47, 51 | sylancl 585 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ≼ {𝑧}) |
53 | 38, 52 | eqbrtrd 5188 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ( I ‘(𝐹 “ {𝑧})) ≼ {𝑧}) |
54 | | simplr 768 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ¬ 𝑧 ∈ 𝑦) |
55 | | disjsn 4736 |
. . . . . . . . 9
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦) |
56 | 54, 55 | sylibr 234 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝑦 ∩ {𝑧}) = ∅) |
57 | | undom 9125 |
. . . . . . . 8
⊢ ((((𝐹 “ 𝑦) ≼ 𝑦 ∧ ( I ‘(𝐹 “ {𝑧})) ≼ {𝑧}) ∧ (𝑦 ∩ {𝑧}) = ∅) → ((𝐹 “ 𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) ≼ (𝑦 ∪ {𝑧})) |
58 | 42, 53, 56, 57 | syl21anc 837 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ((𝐹 “ 𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) ≼ (𝑦 ∪ {𝑧})) |
59 | 41, 58 | eqbrtrrd 5190 |
. . . . . 6
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧})) |
60 | 59 | exp32 420 |
. . . . 5
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝐹 Fn 𝐴 → ((𝐹 “ 𝑦) ≼ 𝑦 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧})))) |
61 | 60 | a2d 29 |
. . . 4
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐹 Fn 𝐴 → (𝐹 “ 𝑦) ≼ 𝑦) → (𝐹 Fn 𝐴 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧})))) |
62 | 8, 12, 16, 20, 23, 61 | findcard2s 9231 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) ≼ 𝐴)) |
63 | | fofn 6836 |
. . 3
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴) |
64 | 62, 63 | impel 505 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → (𝐹 “ 𝐴) ≼ 𝐴) |
65 | 2, 64 | eqbrtrrd 5190 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴) |