Step | Hyp | Ref
| Expression |
1 | | foima 6033 |
. . 3
⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵) |
2 | 1 | adantl 481 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → (𝐹 “ 𝐴) = 𝐵) |
3 | | fofn 6030 |
. . . 4
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴) |
4 | | imaeq2 5381 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝐹 “ 𝑥) = (𝐹 “ ∅)) |
5 | | ima0 5400 |
. . . . . . . 8
⊢ (𝐹 “ ∅) =
∅ |
6 | 4, 5 | syl6eq 2660 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝐹 “ 𝑥) = ∅) |
7 | | id 22 |
. . . . . . 7
⊢ (𝑥 = ∅ → 𝑥 = ∅) |
8 | 6, 7 | breq12d 4596 |
. . . . . 6
⊢ (𝑥 = ∅ → ((𝐹 “ 𝑥) ≼ 𝑥 ↔ ∅ ≼
∅)) |
9 | 8 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐹 Fn 𝐴 → (𝐹 “ 𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → ∅ ≼
∅))) |
10 | | imaeq2 5381 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐹 “ 𝑥) = (𝐹 “ 𝑦)) |
11 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
12 | 10, 11 | breq12d 4596 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝐹 “ 𝑥) ≼ 𝑥 ↔ (𝐹 “ 𝑦) ≼ 𝑦)) |
13 | 12 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐹 Fn 𝐴 → (𝐹 “ 𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹 “ 𝑦) ≼ 𝑦))) |
14 | | imaeq2 5381 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹 “ 𝑥) = (𝐹 “ (𝑦 ∪ {𝑧}))) |
15 | | id 22 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → 𝑥 = (𝑦 ∪ {𝑧})) |
16 | 14, 15 | breq12d 4596 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐹 “ 𝑥) ≼ 𝑥 ↔ (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧}))) |
17 | 16 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐹 Fn 𝐴 → (𝐹 “ 𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧})))) |
18 | | imaeq2 5381 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐹 “ 𝑥) = (𝐹 “ 𝐴)) |
19 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) |
20 | 18, 19 | breq12d 4596 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝐹 “ 𝑥) ≼ 𝑥 ↔ (𝐹 “ 𝐴) ≼ 𝐴)) |
21 | 20 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝐹 Fn 𝐴 → (𝐹 “ 𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) ≼ 𝐴))) |
22 | | 0ex 4718 |
. . . . . . 7
⊢ ∅
∈ V |
23 | 22 | 0dom 7975 |
. . . . . 6
⊢ ∅
≼ ∅ |
24 | 23 | a1i 11 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → ∅ ≼
∅) |
25 | | fnfun 5902 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 Fn 𝐴 → Fun 𝐹) |
26 | 25 | ad2antrl 760 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → Fun 𝐹) |
27 | | funressn 6331 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 → (𝐹 ↾ {𝑧}) ⊆ {〈𝑧, (𝐹‘𝑧)〉}) |
28 | | rnss 5275 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ↾ {𝑧}) ⊆ {〈𝑧, (𝐹‘𝑧)〉} → ran (𝐹 ↾ {𝑧}) ⊆ ran {〈𝑧, (𝐹‘𝑧)〉}) |
29 | 26, 27, 28 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ran (𝐹 ↾ {𝑧}) ⊆ ran {〈𝑧, (𝐹‘𝑧)〉}) |
30 | | df-ima 5051 |
. . . . . . . . . . . . 13
⊢ (𝐹 “ {𝑧}) = ran (𝐹 ↾ {𝑧}) |
31 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V |
32 | 31 | rnsnop 5534 |
. . . . . . . . . . . . . 14
⊢ ran
{〈𝑧, (𝐹‘𝑧)〉} = {(𝐹‘𝑧)} |
33 | 32 | eqcomi 2619 |
. . . . . . . . . . . . 13
⊢ {(𝐹‘𝑧)} = ran {〈𝑧, (𝐹‘𝑧)〉} |
34 | 29, 30, 33 | 3sstr4g 3609 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ⊆ {(𝐹‘𝑧)}) |
35 | | snex 4835 |
. . . . . . . . . . . 12
⊢ {(𝐹‘𝑧)} ∈ V |
36 | | ssexg 4732 |
. . . . . . . . . . . 12
⊢ (((𝐹 “ {𝑧}) ⊆ {(𝐹‘𝑧)} ∧ {(𝐹‘𝑧)} ∈ V) → (𝐹 “ {𝑧}) ∈ V) |
37 | 34, 35, 36 | sylancl 693 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ∈ V) |
38 | | fvi 6165 |
. . . . . . . . . . 11
⊢ ((𝐹 “ {𝑧}) ∈ V → ( I ‘(𝐹 “ {𝑧})) = (𝐹 “ {𝑧})) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ( I ‘(𝐹 “ {𝑧})) = (𝐹 “ {𝑧})) |
40 | 39 | uneq2d 3729 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ((𝐹 “ 𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) = ((𝐹 “ 𝑦) ∪ (𝐹 “ {𝑧}))) |
41 | | imaundi 5464 |
. . . . . . . . 9
⊢ (𝐹 “ (𝑦 ∪ {𝑧})) = ((𝐹 “ 𝑦) ∪ (𝐹 “ {𝑧})) |
42 | 40, 41 | syl6eqr 2662 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ((𝐹 “ 𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) = (𝐹 “ (𝑦 ∪ {𝑧}))) |
43 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ 𝑦) ≼ 𝑦) |
44 | | ssdomg 7887 |
. . . . . . . . . . . 12
⊢ ({(𝐹‘𝑧)} ∈ V → ((𝐹 “ {𝑧}) ⊆ {(𝐹‘𝑧)} → (𝐹 “ {𝑧}) ≼ {(𝐹‘𝑧)})) |
45 | 35, 34, 44 | mpsyl 66 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ≼ {(𝐹‘𝑧)}) |
46 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (𝐹‘𝑧) ∈ V |
47 | 46 | ensn1 7906 |
. . . . . . . . . . . 12
⊢ {(𝐹‘𝑧)} ≈
1𝑜 |
48 | 31 | ensn1 7906 |
. . . . . . . . . . . 12
⊢ {𝑧} ≈
1𝑜 |
49 | 47, 48 | entr4i 7899 |
. . . . . . . . . . 11
⊢ {(𝐹‘𝑧)} ≈ {𝑧} |
50 | | domentr 7901 |
. . . . . . . . . . 11
⊢ (((𝐹 “ {𝑧}) ≼ {(𝐹‘𝑧)} ∧ {(𝐹‘𝑧)} ≈ {𝑧}) → (𝐹 “ {𝑧}) ≼ {𝑧}) |
51 | 45, 49, 50 | sylancl 693 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ≼ {𝑧}) |
52 | 39, 51 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ( I ‘(𝐹 “ {𝑧})) ≼ {𝑧}) |
53 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ¬ 𝑧 ∈ 𝑦) |
54 | | disjsn 4192 |
. . . . . . . . . 10
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦) |
55 | 53, 54 | sylibr 223 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝑦 ∩ {𝑧}) = ∅) |
56 | | undom 7933 |
. . . . . . . . 9
⊢ ((((𝐹 “ 𝑦) ≼ 𝑦 ∧ ( I ‘(𝐹 “ {𝑧})) ≼ {𝑧}) ∧ (𝑦 ∩ {𝑧}) = ∅) → ((𝐹 “ 𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) ≼ (𝑦 ∪ {𝑧})) |
57 | 43, 52, 55, 56 | syl21anc 1317 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ((𝐹 “ 𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) ≼ (𝑦 ∪ {𝑧})) |
58 | 42, 57 | eqbrtrrd 4607 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧})) |
59 | 58 | exp32 629 |
. . . . . 6
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝐹 Fn 𝐴 → ((𝐹 “ 𝑦) ≼ 𝑦 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧})))) |
60 | 59 | a2d 29 |
. . . . 5
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐹 Fn 𝐴 → (𝐹 “ 𝑦) ≼ 𝑦) → (𝐹 Fn 𝐴 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧})))) |
61 | 9, 13, 17, 21, 24, 60 | findcard2s 8086 |
. . . 4
⊢ (𝐴 ∈ Fin → (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) ≼ 𝐴)) |
62 | 3, 61 | syl5 33 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) ≼ 𝐴)) |
63 | 62 | imp 444 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → (𝐹 “ 𝐴) ≼ 𝐴) |
64 | 2, 63 | eqbrtrrd 4607 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴) |