Proof of Theorem subfacp1lem4
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | derang.d | . . . . 5
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)})) | 
| 2 |  | subfac.n | . . . . 5
⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛))) | 
| 3 |  | subfacp1lem.a | . . . . 5
⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)} | 
| 4 |  | subfacp1lem1.n | . . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 5 |  | subfacp1lem1.m | . . . . 5
⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1))) | 
| 6 |  | subfacp1lem1.x | . . . . 5
⊢ 𝑀 ∈ V | 
| 7 |  | subfacp1lem1.k | . . . . 5
⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀}) | 
| 8 |  | subfacp1lem5.f | . . . . 5
⊢ 𝐹 = (( I ↾ 𝐾) ∪ {〈1, 𝑀〉, 〈𝑀, 1〉}) | 
| 9 |  | f1oi 6886 | . . . . . 6
⊢ ( I
↾ 𝐾):𝐾–1-1-onto→𝐾 | 
| 10 | 9 | a1i 11 | . . . . 5
⊢ (𝜑 → ( I ↾ 𝐾):𝐾–1-1-onto→𝐾) | 
| 11 | 1, 2, 3, 4, 5, 6, 7, 8, 10 | subfacp1lem2a 35185 | . . . 4
⊢ (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹‘𝑀) = 1)) | 
| 12 | 11 | simp1d 1143 | . . 3
⊢ (𝜑 → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))) | 
| 13 |  | f1ocnv 6860 | . . 3
⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ◡𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))) | 
| 14 |  | f1ofn 6849 | . . 3
⊢ (◡𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ◡𝐹 Fn (1...(𝑁 + 1))) | 
| 15 | 12, 13, 14 | 3syl 18 | . 2
⊢ (𝜑 → ◡𝐹 Fn (1...(𝑁 + 1))) | 
| 16 |  | f1ofn 6849 | . . 3
⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹 Fn (1...(𝑁 + 1))) | 
| 17 | 12, 16 | syl 17 | . 2
⊢ (𝜑 → 𝐹 Fn (1...(𝑁 + 1))) | 
| 18 | 1, 2, 3, 4, 5, 6, 7 | subfacp1lem1 35184 | . . . . . . . 8
⊢ (𝜑 → ((𝐾 ∩ {1, 𝑀}) = ∅ ∧ (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) ∧ (♯‘𝐾) = (𝑁 − 1))) | 
| 19 | 18 | simp2d 1144 | . . . . . . 7
⊢ (𝜑 → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1))) | 
| 20 | 19 | eleq2d 2827 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐾 ∪ {1, 𝑀}) ↔ 𝑥 ∈ (1...(𝑁 + 1)))) | 
| 21 | 20 | biimpar 477 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝑁 + 1))) → 𝑥 ∈ (𝐾 ∪ {1, 𝑀})) | 
| 22 |  | elun 4153 | . . . . 5
⊢ (𝑥 ∈ (𝐾 ∪ {1, 𝑀}) ↔ (𝑥 ∈ 𝐾 ∨ 𝑥 ∈ {1, 𝑀})) | 
| 23 | 21, 22 | sylib 218 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝑁 + 1))) → (𝑥 ∈ 𝐾 ∨ 𝑥 ∈ {1, 𝑀})) | 
| 24 | 1, 2, 3, 4, 5, 6, 7, 8, 10 | subfacp1lem2b 35186 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐹‘𝑥) = (( I ↾ 𝐾)‘𝑥)) | 
| 25 |  | fvresi 7193 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐾 → (( I ↾ 𝐾)‘𝑥) = 𝑥) | 
| 26 | 25 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (( I ↾ 𝐾)‘𝑥) = 𝑥) | 
| 27 | 24, 26 | eqtrd 2777 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐹‘𝑥) = 𝑥) | 
| 28 | 27 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥)) | 
| 29 | 28, 27 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐹‘(𝐹‘𝑥)) = 𝑥) | 
| 30 |  | vex 3484 | . . . . . . 7
⊢ 𝑥 ∈ V | 
| 31 | 30 | elpr 4650 | . . . . . 6
⊢ (𝑥 ∈ {1, 𝑀} ↔ (𝑥 = 1 ∨ 𝑥 = 𝑀)) | 
| 32 | 11 | simp2d 1144 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘1) = 𝑀) | 
| 33 | 32 | fveq2d 6910 | . . . . . . . . . 10
⊢ (𝜑 → (𝐹‘(𝐹‘1)) = (𝐹‘𝑀)) | 
| 34 | 11 | simp3d 1145 | . . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝑀) = 1) | 
| 35 | 33, 34 | eqtrd 2777 | . . . . . . . . 9
⊢ (𝜑 → (𝐹‘(𝐹‘1)) = 1) | 
| 36 |  | 2fveq3 6911 | . . . . . . . . . 10
⊢ (𝑥 = 1 → (𝐹‘(𝐹‘𝑥)) = (𝐹‘(𝐹‘1))) | 
| 37 |  | id 22 | . . . . . . . . . 10
⊢ (𝑥 = 1 → 𝑥 = 1) | 
| 38 | 36, 37 | eqeq12d 2753 | . . . . . . . . 9
⊢ (𝑥 = 1 → ((𝐹‘(𝐹‘𝑥)) = 𝑥 ↔ (𝐹‘(𝐹‘1)) = 1)) | 
| 39 | 35, 38 | syl5ibrcom 247 | . . . . . . . 8
⊢ (𝜑 → (𝑥 = 1 → (𝐹‘(𝐹‘𝑥)) = 𝑥)) | 
| 40 | 34 | fveq2d 6910 | . . . . . . . . . 10
⊢ (𝜑 → (𝐹‘(𝐹‘𝑀)) = (𝐹‘1)) | 
| 41 | 40, 32 | eqtrd 2777 | . . . . . . . . 9
⊢ (𝜑 → (𝐹‘(𝐹‘𝑀)) = 𝑀) | 
| 42 |  | 2fveq3 6911 | . . . . . . . . . 10
⊢ (𝑥 = 𝑀 → (𝐹‘(𝐹‘𝑥)) = (𝐹‘(𝐹‘𝑀))) | 
| 43 |  | id 22 | . . . . . . . . . 10
⊢ (𝑥 = 𝑀 → 𝑥 = 𝑀) | 
| 44 | 42, 43 | eqeq12d 2753 | . . . . . . . . 9
⊢ (𝑥 = 𝑀 → ((𝐹‘(𝐹‘𝑥)) = 𝑥 ↔ (𝐹‘(𝐹‘𝑀)) = 𝑀)) | 
| 45 | 41, 44 | syl5ibrcom 247 | . . . . . . . 8
⊢ (𝜑 → (𝑥 = 𝑀 → (𝐹‘(𝐹‘𝑥)) = 𝑥)) | 
| 46 | 39, 45 | jaod 860 | . . . . . . 7
⊢ (𝜑 → ((𝑥 = 1 ∨ 𝑥 = 𝑀) → (𝐹‘(𝐹‘𝑥)) = 𝑥)) | 
| 47 | 46 | imp 406 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 1 ∨ 𝑥 = 𝑀)) → (𝐹‘(𝐹‘𝑥)) = 𝑥) | 
| 48 | 31, 47 | sylan2b 594 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ {1, 𝑀}) → (𝐹‘(𝐹‘𝑥)) = 𝑥) | 
| 49 | 29, 48 | jaodan 960 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∨ 𝑥 ∈ {1, 𝑀})) → (𝐹‘(𝐹‘𝑥)) = 𝑥) | 
| 50 | 23, 49 | syldan 591 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝑁 + 1))) → (𝐹‘(𝐹‘𝑥)) = 𝑥) | 
| 51 | 12 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝑁 + 1))) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1))) | 
| 52 |  | f1of 6848 | . . . . . 6
⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1))) | 
| 53 | 12, 52 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1))) | 
| 54 | 53 | ffvelcdmda 7104 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝑁 + 1))) → (𝐹‘𝑥) ∈ (1...(𝑁 + 1))) | 
| 55 |  | f1ocnvfv 7298 | . . . 4
⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘𝑥) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝐹‘𝑥)) = 𝑥 → (◡𝐹‘𝑥) = (𝐹‘𝑥))) | 
| 56 | 51, 54, 55 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝐹‘𝑥)) = 𝑥 → (◡𝐹‘𝑥) = (𝐹‘𝑥))) | 
| 57 | 50, 56 | mpd 15 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝑁 + 1))) → (◡𝐹‘𝑥) = (𝐹‘𝑥)) | 
| 58 | 15, 17, 57 | eqfnfvd 7054 | 1
⊢ (𝜑 → ◡𝐹 = 𝐹) |