Proof of Theorem dif1enlemOLD
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp1 1136 | . 2
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑀 ∈ ω ∧ 𝐹:𝐴–1-1-onto→suc
𝑀) → 𝐹 ∈ 𝑉) | 
| 2 |  | sucidg 6464 | . . . . . 6
⊢ (𝑀 ∈ ω → 𝑀 ∈ suc 𝑀) | 
| 3 |  | dff1o3 6853 | . . . . . . . . 9
⊢ (𝐹:𝐴–1-1-onto→suc
𝑀 ↔ (𝐹:𝐴–onto→suc 𝑀 ∧ Fun ◡𝐹)) | 
| 4 | 3 | simprbi 496 | . . . . . . . 8
⊢ (𝐹:𝐴–1-1-onto→suc
𝑀 → Fun ◡𝐹) | 
| 5 | 4 | adantr 480 | . . . . . . 7
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → Fun ◡𝐹) | 
| 6 |  | f1ofo 6854 | . . . . . . . . 9
⊢ (𝐹:𝐴–1-1-onto→suc
𝑀 → 𝐹:𝐴–onto→suc 𝑀) | 
| 7 |  | f1ofn 6848 | . . . . . . . . . 10
⊢ (𝐹:𝐴–1-1-onto→suc
𝑀 → 𝐹 Fn 𝐴) | 
| 8 |  | fnresdm 6686 | . . . . . . . . . 10
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) | 
| 9 |  | foeq1 6815 | . . . . . . . . . 10
⊢ ((𝐹 ↾ 𝐴) = 𝐹 → ((𝐹 ↾ 𝐴):𝐴–onto→suc 𝑀 ↔ 𝐹:𝐴–onto→suc 𝑀)) | 
| 10 | 7, 8, 9 | 3syl 18 | . . . . . . . . 9
⊢ (𝐹:𝐴–1-1-onto→suc
𝑀 → ((𝐹 ↾ 𝐴):𝐴–onto→suc 𝑀 ↔ 𝐹:𝐴–onto→suc 𝑀)) | 
| 11 | 6, 10 | mpbird 257 | . . . . . . . 8
⊢ (𝐹:𝐴–1-1-onto→suc
𝑀 → (𝐹 ↾ 𝐴):𝐴–onto→suc 𝑀) | 
| 12 | 11 | adantr 480 | . . . . . . 7
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (𝐹 ↾ 𝐴):𝐴–onto→suc 𝑀) | 
| 13 | 7 | adantr 480 | . . . . . . . . 9
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → 𝐹 Fn 𝐴) | 
| 14 |  | f1ocnvdm 7306 | . . . . . . . . 9
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (◡𝐹‘𝑀) ∈ 𝐴) | 
| 15 |  | f1ocnvfv2 7298 | . . . . . . . . . 10
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (𝐹‘(◡𝐹‘𝑀)) = 𝑀) | 
| 16 |  | snidg 4659 | . . . . . . . . . . 11
⊢ (𝑀 ∈ suc 𝑀 → 𝑀 ∈ {𝑀}) | 
| 17 | 16 | adantl 481 | . . . . . . . . . 10
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → 𝑀 ∈ {𝑀}) | 
| 18 | 15, 17 | eqeltrd 2840 | . . . . . . . . 9
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (𝐹‘(◡𝐹‘𝑀)) ∈ {𝑀}) | 
| 19 |  | fressnfv 7179 | . . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ (◡𝐹‘𝑀) ∈ 𝐴) → ((𝐹 ↾ {(◡𝐹‘𝑀)}):{(◡𝐹‘𝑀)}⟶{𝑀} ↔ (𝐹‘(◡𝐹‘𝑀)) ∈ {𝑀})) | 
| 20 | 19 | biimp3ar 1471 | . . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ (◡𝐹‘𝑀) ∈ 𝐴 ∧ (𝐹‘(◡𝐹‘𝑀)) ∈ {𝑀}) → (𝐹 ↾ {(◡𝐹‘𝑀)}):{(◡𝐹‘𝑀)}⟶{𝑀}) | 
| 21 | 13, 14, 18, 20 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (𝐹 ↾ {(◡𝐹‘𝑀)}):{(◡𝐹‘𝑀)}⟶{𝑀}) | 
| 22 |  | disjsn 4710 | . . . . . . . . . . . 12
⊢ ((𝐴 ∩ {(◡𝐹‘𝑀)}) = ∅ ↔ ¬ (◡𝐹‘𝑀) ∈ 𝐴) | 
| 23 | 22 | con2bii 357 | . . . . . . . . . . 11
⊢ ((◡𝐹‘𝑀) ∈ 𝐴 ↔ ¬ (𝐴 ∩ {(◡𝐹‘𝑀)}) = ∅) | 
| 24 | 14, 23 | sylib 218 | . . . . . . . . . 10
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → ¬ (𝐴 ∩ {(◡𝐹‘𝑀)}) = ∅) | 
| 25 |  | fnresdisj 6687 | . . . . . . . . . . . 12
⊢ (𝐹 Fn 𝐴 → ((𝐴 ∩ {(◡𝐹‘𝑀)}) = ∅ ↔ (𝐹 ↾ {(◡𝐹‘𝑀)}) = ∅)) | 
| 26 | 7, 25 | syl 17 | . . . . . . . . . . 11
⊢ (𝐹:𝐴–1-1-onto→suc
𝑀 → ((𝐴 ∩ {(◡𝐹‘𝑀)}) = ∅ ↔ (𝐹 ↾ {(◡𝐹‘𝑀)}) = ∅)) | 
| 27 | 26 | adantr 480 | . . . . . . . . . 10
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → ((𝐴 ∩ {(◡𝐹‘𝑀)}) = ∅ ↔ (𝐹 ↾ {(◡𝐹‘𝑀)}) = ∅)) | 
| 28 | 24, 27 | mtbid 324 | . . . . . . . . 9
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → ¬ (𝐹 ↾ {(◡𝐹‘𝑀)}) = ∅) | 
| 29 | 28 | neqned 2946 | . . . . . . . 8
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (𝐹 ↾ {(◡𝐹‘𝑀)}) ≠ ∅) | 
| 30 |  | foconst 6834 | . . . . . . . 8
⊢ (((𝐹 ↾ {(◡𝐹‘𝑀)}):{(◡𝐹‘𝑀)}⟶{𝑀} ∧ (𝐹 ↾ {(◡𝐹‘𝑀)}) ≠ ∅) → (𝐹 ↾ {(◡𝐹‘𝑀)}):{(◡𝐹‘𝑀)}–onto→{𝑀}) | 
| 31 | 21, 29, 30 | syl2anc 584 | . . . . . . 7
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (𝐹 ↾ {(◡𝐹‘𝑀)}):{(◡𝐹‘𝑀)}–onto→{𝑀}) | 
| 32 |  | resdif 6868 | . . . . . . 7
⊢ ((Fun
◡𝐹 ∧ (𝐹 ↾ 𝐴):𝐴–onto→suc 𝑀 ∧ (𝐹 ↾ {(◡𝐹‘𝑀)}):{(◡𝐹‘𝑀)}–onto→{𝑀}) → (𝐹 ↾ (𝐴 ∖ {(◡𝐹‘𝑀)})):(𝐴 ∖ {(◡𝐹‘𝑀)})–1-1-onto→(suc
𝑀 ∖ {𝑀})) | 
| 33 | 5, 12, 31, 32 | syl3anc 1372 | . . . . . 6
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (𝐹 ↾ (𝐴 ∖ {(◡𝐹‘𝑀)})):(𝐴 ∖ {(◡𝐹‘𝑀)})–1-1-onto→(suc
𝑀 ∖ {𝑀})) | 
| 34 | 2, 33 | sylan2 593 | . . . . 5
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ ω) → (𝐹 ↾ (𝐴 ∖ {(◡𝐹‘𝑀)})):(𝐴 ∖ {(◡𝐹‘𝑀)})–1-1-onto→(suc
𝑀 ∖ {𝑀})) | 
| 35 |  | nnord 7896 | . . . . . . . 8
⊢ (𝑀 ∈ ω → Ord 𝑀) | 
| 36 |  | orddif 6479 | . . . . . . . 8
⊢ (Ord
𝑀 → 𝑀 = (suc 𝑀 ∖ {𝑀})) | 
| 37 | 35, 36 | syl 17 | . . . . . . 7
⊢ (𝑀 ∈ ω → 𝑀 = (suc 𝑀 ∖ {𝑀})) | 
| 38 | 37 | f1oeq3d 6844 | . . . . . 6
⊢ (𝑀 ∈ ω → ((𝐹 ↾ (𝐴 ∖ {(◡𝐹‘𝑀)})):(𝐴 ∖ {(◡𝐹‘𝑀)})–1-1-onto→𝑀 ↔ (𝐹 ↾ (𝐴 ∖ {(◡𝐹‘𝑀)})):(𝐴 ∖ {(◡𝐹‘𝑀)})–1-1-onto→(suc
𝑀 ∖ {𝑀}))) | 
| 39 | 38 | adantl 481 | . . . . 5
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ ω) → ((𝐹 ↾ (𝐴 ∖ {(◡𝐹‘𝑀)})):(𝐴 ∖ {(◡𝐹‘𝑀)})–1-1-onto→𝑀 ↔ (𝐹 ↾ (𝐴 ∖ {(◡𝐹‘𝑀)})):(𝐴 ∖ {(◡𝐹‘𝑀)})–1-1-onto→(suc
𝑀 ∖ {𝑀}))) | 
| 40 | 34, 39 | mpbird 257 | . . . 4
⊢ ((𝐹:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ ω) → (𝐹 ↾ (𝐴 ∖ {(◡𝐹‘𝑀)})):(𝐴 ∖ {(◡𝐹‘𝑀)})–1-1-onto→𝑀) | 
| 41 | 40 | ancoms 458 | . . 3
⊢ ((𝑀 ∈ ω ∧ 𝐹:𝐴–1-1-onto→suc
𝑀) → (𝐹 ↾ (𝐴 ∖ {(◡𝐹‘𝑀)})):(𝐴 ∖ {(◡𝐹‘𝑀)})–1-1-onto→𝑀) | 
| 42 | 41 | 3adant1 1130 | . 2
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑀 ∈ ω ∧ 𝐹:𝐴–1-1-onto→suc
𝑀) → (𝐹 ↾ (𝐴 ∖ {(◡𝐹‘𝑀)})):(𝐴 ∖ {(◡𝐹‘𝑀)})–1-1-onto→𝑀) | 
| 43 |  | resexg 6044 | . . 3
⊢ (𝐹 ∈ 𝑉 → (𝐹 ↾ (𝐴 ∖ {(◡𝐹‘𝑀)})) ∈ V) | 
| 44 |  | f1oen3g 9008 | . . 3
⊢ (((𝐹 ↾ (𝐴 ∖ {(◡𝐹‘𝑀)})) ∈ V ∧ (𝐹 ↾ (𝐴 ∖ {(◡𝐹‘𝑀)})):(𝐴 ∖ {(◡𝐹‘𝑀)})–1-1-onto→𝑀) → (𝐴 ∖ {(◡𝐹‘𝑀)}) ≈ 𝑀) | 
| 45 | 43, 44 | sylan 580 | . 2
⊢ ((𝐹 ∈ 𝑉 ∧ (𝐹 ↾ (𝐴 ∖ {(◡𝐹‘𝑀)})):(𝐴 ∖ {(◡𝐹‘𝑀)})–1-1-onto→𝑀) → (𝐴 ∖ {(◡𝐹‘𝑀)}) ≈ 𝑀) | 
| 46 | 1, 42, 45 | syl2anc 584 | 1
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑀 ∈ ω ∧ 𝐹:𝐴–1-1-onto→suc
𝑀) → (𝐴 ∖ {(◡𝐹‘𝑀)}) ≈ 𝑀) |