Proof of Theorem subfacp1lem2a
| Step | Hyp | Ref
| Expression |
| 1 | | subfacp1lem2.6 |
. . . 4
⊢ (𝜑 → 𝐺:𝐾–1-1-onto→𝐾) |
| 2 | | 1z 12647 |
. . . . . 6
⊢ 1 ∈
ℤ |
| 3 | | subfacp1lem1.x |
. . . . . 6
⊢ 𝑀 ∈ V |
| 4 | | f1oprswap 6892 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ 𝑀
∈ V) → {〈1, 𝑀〉, 〈𝑀, 1〉}:{1, 𝑀}–1-1-onto→{1,
𝑀}) |
| 5 | 2, 3, 4 | mp2an 692 |
. . . . 5
⊢ {〈1,
𝑀〉, 〈𝑀, 1〉}:{1, 𝑀}–1-1-onto→{1,
𝑀} |
| 6 | 5 | a1i 11 |
. . . 4
⊢ (𝜑 → {〈1, 𝑀〉, 〈𝑀, 1〉}:{1, 𝑀}–1-1-onto→{1,
𝑀}) |
| 7 | | derang.d |
. . . . . 6
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)})) |
| 8 | | subfac.n |
. . . . . 6
⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛))) |
| 9 | | subfacp1lem.a |
. . . . . 6
⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)} |
| 10 | | subfacp1lem1.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 11 | | subfacp1lem1.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1))) |
| 12 | | subfacp1lem1.k |
. . . . . 6
⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀}) |
| 13 | 7, 8, 9, 10, 11, 3, 12 | subfacp1lem1 35184 |
. . . . 5
⊢ (𝜑 → ((𝐾 ∩ {1, 𝑀}) = ∅ ∧ (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) ∧ (♯‘𝐾) = (𝑁 − 1))) |
| 14 | 13 | simp1d 1143 |
. . . 4
⊢ (𝜑 → (𝐾 ∩ {1, 𝑀}) = ∅) |
| 15 | | f1oun 6867 |
. . . 4
⊢ (((𝐺:𝐾–1-1-onto→𝐾 ∧ {〈1, 𝑀〉, 〈𝑀, 1〉}:{1, 𝑀}–1-1-onto→{1,
𝑀}) ∧ ((𝐾 ∩ {1, 𝑀}) = ∅ ∧ (𝐾 ∩ {1, 𝑀}) = ∅)) → (𝐺 ∪ {〈1, 𝑀〉, 〈𝑀, 1〉}):(𝐾 ∪ {1, 𝑀})–1-1-onto→(𝐾 ∪ {1, 𝑀})) |
| 16 | 1, 6, 14, 14, 15 | syl22anc 839 |
. . 3
⊢ (𝜑 → (𝐺 ∪ {〈1, 𝑀〉, 〈𝑀, 1〉}):(𝐾 ∪ {1, 𝑀})–1-1-onto→(𝐾 ∪ {1, 𝑀})) |
| 17 | 13 | simp2d 1144 |
. . . 4
⊢ (𝜑 → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1))) |
| 18 | | subfacp1lem2.5 |
. . . . . . 7
⊢ 𝐹 = (𝐺 ∪ {〈1, 𝑀〉, 〈𝑀, 1〉}) |
| 19 | | f1oeq1 6836 |
. . . . . . 7
⊢ (𝐹 = (𝐺 ∪ {〈1, 𝑀〉, 〈𝑀, 1〉}) → (𝐹:(𝐾 ∪ {1, 𝑀})–1-1-onto→(𝐾 ∪ {1, 𝑀}) ↔ (𝐺 ∪ {〈1, 𝑀〉, 〈𝑀, 1〉}):(𝐾 ∪ {1, 𝑀})–1-1-onto→(𝐾 ∪ {1, 𝑀}))) |
| 20 | 18, 19 | ax-mp 5 |
. . . . . 6
⊢ (𝐹:(𝐾 ∪ {1, 𝑀})–1-1-onto→(𝐾 ∪ {1, 𝑀}) ↔ (𝐺 ∪ {〈1, 𝑀〉, 〈𝑀, 1〉}):(𝐾 ∪ {1, 𝑀})–1-1-onto→(𝐾 ∪ {1, 𝑀})) |
| 21 | | f1oeq2 6837 |
. . . . . 6
⊢ ((𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) → (𝐹:(𝐾 ∪ {1, 𝑀})–1-1-onto→(𝐾 ∪ {1, 𝑀}) ↔ 𝐹:(1...(𝑁 + 1))–1-1-onto→(𝐾 ∪ {1, 𝑀}))) |
| 22 | 20, 21 | bitr3id 285 |
. . . . 5
⊢ ((𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) → ((𝐺 ∪ {〈1, 𝑀〉, 〈𝑀, 1〉}):(𝐾 ∪ {1, 𝑀})–1-1-onto→(𝐾 ∪ {1, 𝑀}) ↔ 𝐹:(1...(𝑁 + 1))–1-1-onto→(𝐾 ∪ {1, 𝑀}))) |
| 23 | | f1oeq3 6838 |
. . . . 5
⊢ ((𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) → (𝐹:(1...(𝑁 + 1))–1-1-onto→(𝐾 ∪ {1, 𝑀}) ↔ 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))) |
| 24 | 22, 23 | bitrd 279 |
. . . 4
⊢ ((𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) → ((𝐺 ∪ {〈1, 𝑀〉, 〈𝑀, 1〉}):(𝐾 ∪ {1, 𝑀})–1-1-onto→(𝐾 ∪ {1, 𝑀}) ↔ 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))) |
| 25 | 17, 24 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐺 ∪ {〈1, 𝑀〉, 〈𝑀, 1〉}):(𝐾 ∪ {1, 𝑀})–1-1-onto→(𝐾 ∪ {1, 𝑀}) ↔ 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))) |
| 26 | 16, 25 | mpbid 232 |
. 2
⊢ (𝜑 → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))) |
| 27 | | f1ofun 6850 |
. . . . 5
⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → Fun 𝐹) |
| 28 | 26, 27 | syl 17 |
. . . 4
⊢ (𝜑 → Fun 𝐹) |
| 29 | | snsspr1 4814 |
. . . . . 6
⊢ {〈1,
𝑀〉} ⊆ {〈1,
𝑀〉, 〈𝑀, 1〉} |
| 30 | | ssun2 4179 |
. . . . . . 7
⊢ {〈1,
𝑀〉, 〈𝑀, 1〉} ⊆ (𝐺 ∪ {〈1, 𝑀〉, 〈𝑀, 1〉}) |
| 31 | 30, 18 | sseqtrri 4033 |
. . . . . 6
⊢ {〈1,
𝑀〉, 〈𝑀, 1〉} ⊆ 𝐹 |
| 32 | 29, 31 | sstri 3993 |
. . . . 5
⊢ {〈1,
𝑀〉} ⊆ 𝐹 |
| 33 | | 1ex 11257 |
. . . . . . 7
⊢ 1 ∈
V |
| 34 | 33 | snid 4662 |
. . . . . 6
⊢ 1 ∈
{1} |
| 35 | 3 | dmsnop 6236 |
. . . . . 6
⊢ dom
{〈1, 𝑀〉} =
{1} |
| 36 | 34, 35 | eleqtrri 2840 |
. . . . 5
⊢ 1 ∈
dom {〈1, 𝑀〉} |
| 37 | | funssfv 6927 |
. . . . 5
⊢ ((Fun
𝐹 ∧ {〈1, 𝑀〉} ⊆ 𝐹 ∧ 1 ∈ dom {〈1,
𝑀〉}) → (𝐹‘1) = ({〈1, 𝑀〉}‘1)) |
| 38 | 32, 36, 37 | mp3an23 1455 |
. . . 4
⊢ (Fun
𝐹 → (𝐹‘1) = ({〈1, 𝑀〉}‘1)) |
| 39 | 28, 38 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹‘1) = ({〈1, 𝑀〉}‘1)) |
| 40 | 33, 3 | fvsn 7201 |
. . 3
⊢
({〈1, 𝑀〉}‘1) = 𝑀 |
| 41 | 39, 40 | eqtrdi 2793 |
. 2
⊢ (𝜑 → (𝐹‘1) = 𝑀) |
| 42 | | snsspr2 4815 |
. . . . . 6
⊢
{〈𝑀, 1〉}
⊆ {〈1, 𝑀〉,
〈𝑀,
1〉} |
| 43 | 42, 31 | sstri 3993 |
. . . . 5
⊢
{〈𝑀, 1〉}
⊆ 𝐹 |
| 44 | 3 | snid 4662 |
. . . . . 6
⊢ 𝑀 ∈ {𝑀} |
| 45 | 33 | dmsnop 6236 |
. . . . . 6
⊢ dom
{〈𝑀, 1〉} = {𝑀} |
| 46 | 44, 45 | eleqtrri 2840 |
. . . . 5
⊢ 𝑀 ∈ dom {〈𝑀, 1〉} |
| 47 | | funssfv 6927 |
. . . . 5
⊢ ((Fun
𝐹 ∧ {〈𝑀, 1〉} ⊆ 𝐹 ∧ 𝑀 ∈ dom {〈𝑀, 1〉}) → (𝐹‘𝑀) = ({〈𝑀, 1〉}‘𝑀)) |
| 48 | 43, 46, 47 | mp3an23 1455 |
. . . 4
⊢ (Fun
𝐹 → (𝐹‘𝑀) = ({〈𝑀, 1〉}‘𝑀)) |
| 49 | 28, 48 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹‘𝑀) = ({〈𝑀, 1〉}‘𝑀)) |
| 50 | 3, 33 | fvsn 7201 |
. . 3
⊢
({〈𝑀,
1〉}‘𝑀) =
1 |
| 51 | 49, 50 | eqtrdi 2793 |
. 2
⊢ (𝜑 → (𝐹‘𝑀) = 1) |
| 52 | 26, 41, 51 | 3jca 1129 |
1
⊢ (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹‘𝑀) = 1)) |