Step | Hyp | Ref
| Expression |
1 | | subfacp1lem2.6 |
. . . 4
⊢ (𝜑 → 𝐺:𝐾–1-1-onto→𝐾) |
2 | | 1z 12538 |
. . . . . 6
⊢ 1 ∈
ℤ |
3 | | subfacp1lem1.x |
. . . . . 6
⊢ 𝑀 ∈ V |
4 | | f1oprswap 6829 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ 𝑀
∈ V) → {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}:{1, 𝑀}–1-1-onto→{1,
𝑀}) |
5 | 2, 3, 4 | mp2an 691 |
. . . . 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 33830 |
. . . . 5
⊢ (𝜑 → ((𝐾 ∩ {1, 𝑀}) = ∅ ∧ (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) ∧ (♯‘𝐾) = (𝑁 − 1))) |
14 | 13 | simp1d 1143 |
. . . 4
⊢ (𝜑 → (𝐾 ∩ {1, 𝑀}) = ∅) |
15 | | f1oun 6804 |
. . . 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 838 |
. . 3
⊢ (𝜑 → (𝐺 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}):(𝐾 ∪ {1, 𝑀})–1-1-onto→(𝐾 ∪ {1, 𝑀})) |
17 | 13 | simp2d 1144 |
. . . 4
⊢ (𝜑 → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1))) |
18 | | subfacp1lem2.5 |
. . . . . . 7
⊢ 𝐹 = (𝐺 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) |
19 | | f1oeq1 6773 |
. . . . . . 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 6774 |
. . . . . 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 6775 |
. . . . 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 231 |
. 2
⊢ (𝜑 → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))) |
27 | | f1ofun 6787 |
. . . . 5
⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → Fun 𝐹) |
28 | 26, 27 | syl 17 |
. . . 4
⊢ (𝜑 → Fun 𝐹) |
29 | | snsspr1 4775 |
. . . . . 6
⊢ {⟨1,
𝑀⟩} ⊆ {⟨1,
𝑀⟩, ⟨𝑀, 1⟩} |
30 | | ssun2 4134 |
. . . . . . 7
⊢ {⟨1,
𝑀⟩, ⟨𝑀, 1⟩} ⊆ (𝐺 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩}) |
31 | 30, 18 | sseqtrri 3982 |
. . . . . 6
⊢ {⟨1,
𝑀⟩, ⟨𝑀, 1⟩} ⊆ 𝐹 |
32 | 29, 31 | sstri 3954 |
. . . . 5
⊢ {⟨1,
𝑀⟩} ⊆ 𝐹 |
33 | | 1ex 11156 |
. . . . . . 7
⊢ 1 ∈
V |
34 | 33 | snid 4623 |
. . . . . 6
⊢ 1 ∈
{1} |
35 | 3 | dmsnop 6169 |
. . . . . 6
⊢ dom
{⟨1, 𝑀⟩} =
{1} |
36 | 34, 35 | eleqtrri 2833 |
. . . . 5
⊢ 1 ∈
dom {⟨1, 𝑀⟩} |
37 | | funssfv 6864 |
. . . . 5
⊢ ((Fun
𝐹 ∧ {⟨1, 𝑀⟩} ⊆ 𝐹 ∧ 1 ∈ dom {⟨1,
𝑀⟩}) → (𝐹‘1) = ({⟨1, 𝑀⟩}‘1)) |
38 | 32, 36, 37 | mp3an23 1454 |
. . . 4
⊢ (Fun
𝐹 → (𝐹‘1) = ({⟨1, 𝑀⟩}‘1)) |
39 | 28, 38 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹‘1) = ({⟨1, 𝑀⟩}‘1)) |
40 | 33, 3 | fvsn 7128 |
. . 3
⊢
({⟨1, 𝑀⟩}‘1) = 𝑀 |
41 | 39, 40 | eqtrdi 2789 |
. 2
⊢ (𝜑 → (𝐹‘1) = 𝑀) |
42 | | snsspr2 4776 |
. . . . . 6
⊢
{⟨𝑀, 1⟩}
⊆ {⟨1, 𝑀⟩,
⟨𝑀,
1⟩} |
43 | 42, 31 | sstri 3954 |
. . . . 5
⊢
{⟨𝑀, 1⟩}
⊆ 𝐹 |
44 | 3 | snid 4623 |
. . . . . 6
⊢ 𝑀 ∈ {𝑀} |
45 | 33 | dmsnop 6169 |
. . . . . 6
⊢ dom
{⟨𝑀, 1⟩} = {𝑀} |
46 | 44, 45 | eleqtrri 2833 |
. . . . 5
⊢ 𝑀 ∈ dom {⟨𝑀, 1⟩} |
47 | | funssfv 6864 |
. . . . 5
⊢ ((Fun
𝐹 ∧ {⟨𝑀, 1⟩} ⊆ 𝐹 ∧ 𝑀 ∈ dom {⟨𝑀, 1⟩}) → (𝐹‘𝑀) = ({⟨𝑀, 1⟩}‘𝑀)) |
48 | 43, 46, 47 | mp3an23 1454 |
. . . 4
⊢ (Fun
𝐹 → (𝐹‘𝑀) = ({⟨𝑀, 1⟩}‘𝑀)) |
49 | 28, 48 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹‘𝑀) = ({⟨𝑀, 1⟩}‘𝑀)) |
50 | 3, 33 | fvsn 7128 |
. . 3
⊢
({⟨𝑀,
1⟩}‘𝑀) =
1 |
51 | 49, 50 | eqtrdi 2789 |
. 2
⊢ (𝜑 → (𝐹‘𝑀) = 1) |
52 | 26, 41, 51 | 3jca 1129 |
1
⊢ (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹‘𝑀) = 1)) |