| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | foima 6824 | . . 3
⊢ (𝐹:𝐴–onto→𝐵 → (𝐹 “ 𝐴) = 𝐵) | 
| 2 | 1 | adantl 481 | . 2
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → (𝐹 “ 𝐴) = 𝐵) | 
| 3 |  | imaeq2 6073 | . . . . . . 7
⊢ (𝑥 = ∅ → (𝐹 “ 𝑥) = (𝐹 “ ∅)) | 
| 4 |  | ima0 6094 | . . . . . . 7
⊢ (𝐹 “ ∅) =
∅ | 
| 5 | 3, 4 | eqtrdi 2792 | . . . . . 6
⊢ (𝑥 = ∅ → (𝐹 “ 𝑥) = ∅) | 
| 6 |  | id 22 | . . . . . 6
⊢ (𝑥 = ∅ → 𝑥 = ∅) | 
| 7 | 5, 6 | breq12d 5155 | . . . . 5
⊢ (𝑥 = ∅ → ((𝐹 “ 𝑥) ≼ 𝑥 ↔ ∅ ≼
∅)) | 
| 8 | 7 | imbi2d 340 | . . . 4
⊢ (𝑥 = ∅ → ((𝐹 Fn 𝐴 → (𝐹 “ 𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → ∅ ≼
∅))) | 
| 9 |  | imaeq2 6073 | . . . . . 6
⊢ (𝑥 = 𝑦 → (𝐹 “ 𝑥) = (𝐹 “ 𝑦)) | 
| 10 |  | id 22 | . . . . . 6
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) | 
| 11 | 9, 10 | breq12d 5155 | . . . . 5
⊢ (𝑥 = 𝑦 → ((𝐹 “ 𝑥) ≼ 𝑥 ↔ (𝐹 “ 𝑦) ≼ 𝑦)) | 
| 12 | 11 | imbi2d 340 | . . . 4
⊢ (𝑥 = 𝑦 → ((𝐹 Fn 𝐴 → (𝐹 “ 𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹 “ 𝑦) ≼ 𝑦))) | 
| 13 |  | imaeq2 6073 | . . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹 “ 𝑥) = (𝐹 “ (𝑦 ∪ {𝑧}))) | 
| 14 |  | id 22 | . . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → 𝑥 = (𝑦 ∪ {𝑧})) | 
| 15 | 13, 14 | breq12d 5155 | . . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐹 “ 𝑥) ≼ 𝑥 ↔ (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧}))) | 
| 16 | 15 | imbi2d 340 | . . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐹 Fn 𝐴 → (𝐹 “ 𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹 “ (𝑦 ∪ {𝑧})) ≼ (𝑦 ∪ {𝑧})))) | 
| 17 |  | imaeq2 6073 | . . . . . 6
⊢ (𝑥 = 𝐴 → (𝐹 “ 𝑥) = (𝐹 “ 𝐴)) | 
| 18 |  | id 22 | . . . . . 6
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) | 
| 19 | 17, 18 | breq12d 5155 | . . . . 5
⊢ (𝑥 = 𝐴 → ((𝐹 “ 𝑥) ≼ 𝑥 ↔ (𝐹 “ 𝐴) ≼ 𝐴)) | 
| 20 | 19 | imbi2d 340 | . . . 4
⊢ (𝑥 = 𝐴 → ((𝐹 Fn 𝐴 → (𝐹 “ 𝑥) ≼ 𝑥) ↔ (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) ≼ 𝐴))) | 
| 21 |  | 0ex 5306 | . . . . . 6
⊢ ∅
∈ V | 
| 22 | 21 | 0dom 9147 | . . . . 5
⊢ ∅
≼ ∅ | 
| 23 | 22 | a1i 11 | . . . 4
⊢ (𝐹 Fn 𝐴 → ∅ ≼
∅) | 
| 24 |  | fnfun 6667 | . . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | 
| 25 | 24 | ad2antrl 728 | . . . . . . . . . . . . 13
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → Fun 𝐹) | 
| 26 |  | funressn 7178 | . . . . . . . . . . . . 13
⊢ (Fun
𝐹 → (𝐹 ↾ {𝑧}) ⊆ {〈𝑧, (𝐹‘𝑧)〉}) | 
| 27 |  | rnss 5949 | . . . . . . . . . . . . 13
⊢ ((𝐹 ↾ {𝑧}) ⊆ {〈𝑧, (𝐹‘𝑧)〉} → ran (𝐹 ↾ {𝑧}) ⊆ ran {〈𝑧, (𝐹‘𝑧)〉}) | 
| 28 | 25, 26, 27 | 3syl 18 | . . . . . . . . . . . 12
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ran (𝐹 ↾ {𝑧}) ⊆ ran {〈𝑧, (𝐹‘𝑧)〉}) | 
| 29 |  | df-ima 5697 | . . . . . . . . . . . 12
⊢ (𝐹 “ {𝑧}) = ran (𝐹 ↾ {𝑧}) | 
| 30 |  | vex 3483 | . . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V | 
| 31 | 30 | rnsnop 6243 | . . . . . . . . . . . . 13
⊢ ran
{〈𝑧, (𝐹‘𝑧)〉} = {(𝐹‘𝑧)} | 
| 32 | 31 | eqcomi 2745 | . . . . . . . . . . . 12
⊢ {(𝐹‘𝑧)} = ran {〈𝑧, (𝐹‘𝑧)〉} | 
| 33 | 28, 29, 32 | 3sstr4g 4036 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ⊆ {(𝐹‘𝑧)}) | 
| 34 |  | snfi 9084 | . . . . . . . . . . 11
⊢ {(𝐹‘𝑧)} ∈ Fin | 
| 35 |  | ssexg 5322 | . . . . . . . . . . 11
⊢ (((𝐹 “ {𝑧}) ⊆ {(𝐹‘𝑧)} ∧ {(𝐹‘𝑧)} ∈ Fin) → (𝐹 “ {𝑧}) ∈ V) | 
| 36 | 33, 34, 35 | sylancl 586 | . . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ∈ V) | 
| 37 |  | fvi 6984 | . . . . . . . . . 10
⊢ ((𝐹 “ {𝑧}) ∈ V → ( I ‘(𝐹 “ {𝑧})) = (𝐹 “ {𝑧})) | 
| 38 | 36, 37 | syl 17 | . . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ( I ‘(𝐹 “ {𝑧})) = (𝐹 “ {𝑧})) | 
| 39 | 38 | uneq2d 4167 | . . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ((𝐹 “ 𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) = ((𝐹 “ 𝑦) ∪ (𝐹 “ {𝑧}))) | 
| 40 |  | imaundi 6168 | . . . . . . . 8
⊢ (𝐹 “ (𝑦 ∪ {𝑧})) = ((𝐹 “ 𝑦) ∪ (𝐹 “ {𝑧})) | 
| 41 | 39, 40 | eqtr4di 2794 | . . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ((𝐹 “ 𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) = (𝐹 “ (𝑦 ∪ {𝑧}))) | 
| 42 |  | simprr 772 | . . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ 𝑦) ≼ 𝑦) | 
| 43 |  | ssdomfi 9237 | . . . . . . . . . . 11
⊢ ({(𝐹‘𝑧)} ∈ Fin → ((𝐹 “ {𝑧}) ⊆ {(𝐹‘𝑧)} → (𝐹 “ {𝑧}) ≼ {(𝐹‘𝑧)})) | 
| 44 | 34, 33, 43 | mpsyl 68 | . . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ≼ {(𝐹‘𝑧)}) | 
| 45 |  | fvex 6918 | . . . . . . . . . . 11
⊢ (𝐹‘𝑧) ∈ V | 
| 46 |  | en2sn 9082 | . . . . . . . . . . 11
⊢ (((𝐹‘𝑧) ∈ V ∧ 𝑧 ∈ V) → {(𝐹‘𝑧)} ≈ {𝑧}) | 
| 47 | 45, 30, 46 | mp2an 692 | . . . . . . . . . 10
⊢ {(𝐹‘𝑧)} ≈ {𝑧} | 
| 48 |  | endom 9020 | . . . . . . . . . . 11
⊢ ({(𝐹‘𝑧)} ≈ {𝑧} → {(𝐹‘𝑧)} ≼ {𝑧}) | 
| 49 |  | domtrfi 9234 | . . . . . . . . . . . 12
⊢ (({(𝐹‘𝑧)} ∈ Fin ∧ (𝐹 “ {𝑧}) ≼ {(𝐹‘𝑧)} ∧ {(𝐹‘𝑧)} ≼ {𝑧}) → (𝐹 “ {𝑧}) ≼ {𝑧}) | 
| 50 | 34, 49 | mp3an1 1449 | . . . . . . . . . . 11
⊢ (((𝐹 “ {𝑧}) ≼ {(𝐹‘𝑧)} ∧ {(𝐹‘𝑧)} ≼ {𝑧}) → (𝐹 “ {𝑧}) ≼ {𝑧}) | 
| 51 | 48, 50 | sylan2 593 | . . . . . . . . . 10
⊢ (((𝐹 “ {𝑧}) ≼ {(𝐹‘𝑧)} ∧ {(𝐹‘𝑧)} ≈ {𝑧}) → (𝐹 “ {𝑧}) ≼ {𝑧}) | 
| 52 | 44, 47, 51 | sylancl 586 | . . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝐹 “ {𝑧}) ≼ {𝑧}) | 
| 53 | 38, 52 | eqbrtrd 5164 | . . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ( I ‘(𝐹 “ {𝑧})) ≼ {𝑧}) | 
| 54 |  | simplr 768 | . . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ¬ 𝑧 ∈ 𝑦) | 
| 55 |  | disjsn 4710 | . . . . . . . . 9
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦) | 
| 56 | 54, 55 | sylibr 234 | . . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → (𝑦 ∩ {𝑧}) = ∅) | 
| 57 |  | undom 9100 | . . . . . . . 8
⊢ ((((𝐹 “ 𝑦) ≼ 𝑦 ∧ ( I ‘(𝐹 “ {𝑧})) ≼ {𝑧}) ∧ (𝑦 ∩ {𝑧}) = ∅) → ((𝐹 “ 𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) ≼ (𝑦 ∪ {𝑧})) | 
| 58 | 42, 53, 56, 57 | syl21anc 837 | . . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐹 Fn 𝐴 ∧ (𝐹 “ 𝑦) ≼ 𝑦)) → ((𝐹 “ 𝑦) ∪ ( I ‘(𝐹 “ {𝑧}))) ≼ (𝑦 ∪ {𝑧})) | 
| 59 | 41, 58 | eqbrtrrd 5166 | . . . . . 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 9206 | . . 3
⊢ (𝐴 ∈ Fin → (𝐹 Fn 𝐴 → (𝐹 “ 𝐴) ≼ 𝐴)) | 
| 63 |  | fofn 6821 | . . 3
⊢ (𝐹:𝐴–onto→𝐵 → 𝐹 Fn 𝐴) | 
| 64 | 62, 63 | impel 505 | . 2
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → (𝐹 “ 𝐴) ≼ 𝐴) | 
| 65 | 2, 64 | eqbrtrrd 5166 | 1
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴) |