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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 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	⊢ ( 𝜑 → ◡ 𝐹 = 𝐹 )