Metamath Proof Explorer


Theorem subfacp1lem4

Description: Lemma for subfacp1 . The function F , which swaps 1 with M and leaves all other elements alone, is a bijection of order 2 , i.e. it is its own inverse. (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypotheses derang.d 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥1-1-onto𝑥 ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) ≠ 𝑦 ) } ) )
subfac.n 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
subfacp1lem.a 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓𝑦 ) ≠ 𝑦 ) }
subfacp1lem1.n ( 𝜑𝑁 ∈ ℕ )
subfacp1lem1.m ( 𝜑𝑀 ∈ ( 2 ... ( 𝑁 + 1 ) ) )
subfacp1lem1.x 𝑀 ∈ V
subfacp1lem1.k 𝐾 = ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } )
subfacp1lem5.b 𝐵 = { 𝑔𝐴 ∣ ( ( 𝑔 ‘ 1 ) = 𝑀 ∧ ( 𝑔𝑀 ) ≠ 1 ) }
subfacp1lem5.f 𝐹 = ( ( I ↾ 𝐾 ) ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } )
Assertion subfacp1lem4 ( 𝜑 𝐹 = 𝐹 )

Proof

Step Hyp Ref Expression
1 derang.d 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥1-1-onto𝑥 ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) ≠ 𝑦 ) } ) )
2 subfac.n 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
3 subfacp1lem.a 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓𝑦 ) ≠ 𝑦 ) }
4 subfacp1lem1.n ( 𝜑𝑁 ∈ ℕ )
5 subfacp1lem1.m ( 𝜑𝑀 ∈ ( 2 ... ( 𝑁 + 1 ) ) )
6 subfacp1lem1.x 𝑀 ∈ V
7 subfacp1lem1.k 𝐾 = ( ( 2 ... ( 𝑁 + 1 ) ) ∖ { 𝑀 } )
8 subfacp1lem5.b 𝐵 = { 𝑔𝐴 ∣ ( ( 𝑔 ‘ 1 ) = 𝑀 ∧ ( 𝑔𝑀 ) ≠ 1 ) }
9 subfacp1lem5.f 𝐹 = ( ( I ↾ 𝐾 ) ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } )
10 f1oi ( I ↾ 𝐾 ) : 𝐾1-1-onto𝐾
11 10 a1i ( 𝜑 → ( I ↾ 𝐾 ) : 𝐾1-1-onto𝐾 )
12 1 2 3 4 5 6 7 9 11 subfacp1lem2a ( 𝜑 → ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( 𝐹 ‘ 1 ) = 𝑀 ∧ ( 𝐹𝑀 ) = 1 ) )
13 12 simp1d ( 𝜑𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
14 f1ocnv ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
15 f1ofn ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → 𝐹 Fn ( 1 ... ( 𝑁 + 1 ) ) )
16 13 14 15 3syl ( 𝜑 𝐹 Fn ( 1 ... ( 𝑁 + 1 ) ) )
17 f1ofn ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → 𝐹 Fn ( 1 ... ( 𝑁 + 1 ) ) )
18 13 17 syl ( 𝜑𝐹 Fn ( 1 ... ( 𝑁 + 1 ) ) )
19 1 2 3 4 5 6 7 subfacp1lem1 ( 𝜑 → ( ( 𝐾 ∩ { 1 , 𝑀 } ) = ∅ ∧ ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) ∧ ( ♯ ‘ 𝐾 ) = ( 𝑁 − 1 ) ) )
20 19 simp2d ( 𝜑 → ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) )
21 20 eleq2d ( 𝜑 → ( 𝑥 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ↔ 𝑥 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) )
22 21 biimpar ( ( 𝜑𝑥 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑥 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) )
23 elun ( 𝑥 ∈ ( 𝐾 ∪ { 1 , 𝑀 } ) ↔ ( 𝑥𝐾𝑥 ∈ { 1 , 𝑀 } ) )
24 22 23 sylib ( ( 𝜑𝑥 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑥𝐾𝑥 ∈ { 1 , 𝑀 } ) )
25 1 2 3 4 5 6 7 9 11 subfacp1lem2b ( ( 𝜑𝑥𝐾 ) → ( 𝐹𝑥 ) = ( ( I ↾ 𝐾 ) ‘ 𝑥 ) )
26 fvresi ( 𝑥𝐾 → ( ( I ↾ 𝐾 ) ‘ 𝑥 ) = 𝑥 )
27 26 adantl ( ( 𝜑𝑥𝐾 ) → ( ( I ↾ 𝐾 ) ‘ 𝑥 ) = 𝑥 )
28 25 27 eqtrd ( ( 𝜑𝑥𝐾 ) → ( 𝐹𝑥 ) = 𝑥 )
29 28 fveq2d ( ( 𝜑𝑥𝐾 ) → ( 𝐹 ‘ ( 𝐹𝑥 ) ) = ( 𝐹𝑥 ) )
30 29 28 eqtrd ( ( 𝜑𝑥𝐾 ) → ( 𝐹 ‘ ( 𝐹𝑥 ) ) = 𝑥 )
31 vex 𝑥 ∈ V
32 31 elpr ( 𝑥 ∈ { 1 , 𝑀 } ↔ ( 𝑥 = 1 ∨ 𝑥 = 𝑀 ) )
33 12 simp2d ( 𝜑 → ( 𝐹 ‘ 1 ) = 𝑀 )
34 33 fveq2d ( 𝜑 → ( 𝐹 ‘ ( 𝐹 ‘ 1 ) ) = ( 𝐹𝑀 ) )
35 12 simp3d ( 𝜑 → ( 𝐹𝑀 ) = 1 )
36 34 35 eqtrd ( 𝜑 → ( 𝐹 ‘ ( 𝐹 ‘ 1 ) ) = 1 )
37 2fveq3 ( 𝑥 = 1 → ( 𝐹 ‘ ( 𝐹𝑥 ) ) = ( 𝐹 ‘ ( 𝐹 ‘ 1 ) ) )
38 id ( 𝑥 = 1 → 𝑥 = 1 )
39 37 38 eqeq12d ( 𝑥 = 1 → ( ( 𝐹 ‘ ( 𝐹𝑥 ) ) = 𝑥 ↔ ( 𝐹 ‘ ( 𝐹 ‘ 1 ) ) = 1 ) )
40 36 39 syl5ibrcom ( 𝜑 → ( 𝑥 = 1 → ( 𝐹 ‘ ( 𝐹𝑥 ) ) = 𝑥 ) )
41 35 fveq2d ( 𝜑 → ( 𝐹 ‘ ( 𝐹𝑀 ) ) = ( 𝐹 ‘ 1 ) )
42 41 33 eqtrd ( 𝜑 → ( 𝐹 ‘ ( 𝐹𝑀 ) ) = 𝑀 )
43 2fveq3 ( 𝑥 = 𝑀 → ( 𝐹 ‘ ( 𝐹𝑥 ) ) = ( 𝐹 ‘ ( 𝐹𝑀 ) ) )
44 id ( 𝑥 = 𝑀𝑥 = 𝑀 )
45 43 44 eqeq12d ( 𝑥 = 𝑀 → ( ( 𝐹 ‘ ( 𝐹𝑥 ) ) = 𝑥 ↔ ( 𝐹 ‘ ( 𝐹𝑀 ) ) = 𝑀 ) )
46 42 45 syl5ibrcom ( 𝜑 → ( 𝑥 = 𝑀 → ( 𝐹 ‘ ( 𝐹𝑥 ) ) = 𝑥 ) )
47 40 46 jaod ( 𝜑 → ( ( 𝑥 = 1 ∨ 𝑥 = 𝑀 ) → ( 𝐹 ‘ ( 𝐹𝑥 ) ) = 𝑥 ) )
48 47 imp ( ( 𝜑 ∧ ( 𝑥 = 1 ∨ 𝑥 = 𝑀 ) ) → ( 𝐹 ‘ ( 𝐹𝑥 ) ) = 𝑥 )
49 32 48 sylan2b ( ( 𝜑𝑥 ∈ { 1 , 𝑀 } ) → ( 𝐹 ‘ ( 𝐹𝑥 ) ) = 𝑥 )
50 30 49 jaodan ( ( 𝜑 ∧ ( 𝑥𝐾𝑥 ∈ { 1 , 𝑀 } ) ) → ( 𝐹 ‘ ( 𝐹𝑥 ) ) = 𝑥 )
51 24 50 syldan ( ( 𝜑𝑥 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ ( 𝐹𝑥 ) ) = 𝑥 )
52 13 adantr ( ( 𝜑𝑥 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
53 f1of ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) )
54 13 53 syl ( 𝜑𝐹 : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ( 1 ... ( 𝑁 + 1 ) ) )
55 54 ffvelrnda ( ( 𝜑𝑥 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝐹𝑥 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) )
56 f1ocnvfv ( ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( 𝐹𝑥 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ‘ ( 𝐹𝑥 ) ) = 𝑥 → ( 𝐹𝑥 ) = ( 𝐹𝑥 ) ) )
57 52 55 56 syl2anc ( ( 𝜑𝑥 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝐹 ‘ ( 𝐹𝑥 ) ) = 𝑥 → ( 𝐹𝑥 ) = ( 𝐹𝑥 ) ) )
58 51 57 mpd ( ( 𝜑𝑥 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝐹𝑥 ) = ( 𝐹𝑥 ) )
59 16 18 58 eqfnfvd ( 𝜑 𝐹 = 𝐹 )