Theorem subfacp1lem2a

Description: Lemma for subfacp1 . Properties of a bijection on K augmented with the two-element flip to get a bijection on K u. { 1 , M } . (Contributed by Mario Carneiro, 23-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 ) ) ∖ { 𝑀 } )
	subfacp1lem2.5	⊢ 𝐹 = ( 𝐺 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } )
	subfacp1lem2.6	⊢ ( 𝜑 → 𝐺 : 𝐾 –1-1-onto→ 𝐾 )
Assertion	subfacp1lem2a	⊢ ( 𝜑 → ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( 𝐹 ‘ 1 ) = 𝑀 ∧ ( 𝐹 ‘ 𝑀 ) = 1 ) )

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		subfacp1lem2.5	⊢ 𝐹 = ( 𝐺 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } )
9		subfacp1lem2.6	⊢ ( 𝜑 → 𝐺 : 𝐾 –1-1-onto→ 𝐾 )
10		1z	⊢ 1 ∈ ℤ
11		f1oprswap	⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ V ) → { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } : { 1 , 𝑀 } –1-1-onto→ { 1 , 𝑀 } )
12	10 6 11	mp2an	⊢ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } : { 1 , 𝑀 } –1-1-onto→ { 1 , 𝑀 }
13	12	a1i	⊢ ( 𝜑 → { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } : { 1 , 𝑀 } –1-1-onto→ { 1 , 𝑀 } )
14	1 2 3 4 5 6 7	subfacp1lem1	⊢ ( 𝜑 → ( ( 𝐾 ∩ { 1 , 𝑀 } ) = ∅ ∧ ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) ∧ ( ♯ ‘ 𝐾 ) = ( 𝑁 − 1 ) ) )
15	14	simp1d	⊢ ( 𝜑 → ( 𝐾 ∩ { 1 , 𝑀 } ) = ∅ )
16		f1oun	⊢ ( ( ( 𝐺 : 𝐾 –1-1-onto→ 𝐾 ∧ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } : { 1 , 𝑀 } –1-1-onto→ { 1 , 𝑀 } ) ∧ ( ( 𝐾 ∩ { 1 , 𝑀 } ) = ∅ ∧ ( 𝐾 ∩ { 1 , 𝑀 } ) = ∅ ) ) → ( 𝐺 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 𝐾 ∪ { 1 , 𝑀 } ) –1-1-onto→ ( 𝐾 ∪ { 1 , 𝑀 } ) )
17	9 13 15 15 16	syl22anc	⊢ ( 𝜑 → ( 𝐺 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 𝐾 ∪ { 1 , 𝑀 } ) –1-1-onto→ ( 𝐾 ∪ { 1 , 𝑀 } ) )
18	14	simp2d	⊢ ( 𝜑 → ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) )
19		f1oeq1	⊢ ( 𝐹 = ( 𝐺 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) → ( 𝐹 : ( 𝐾 ∪ { 1 , 𝑀 } ) –1-1-onto→ ( 𝐾 ∪ { 1 , 𝑀 } ) ↔ ( 𝐺 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 𝐾 ∪ { 1 , 𝑀 } ) –1-1-onto→ ( 𝐾 ∪ { 1 , 𝑀 } ) ) )
20	8 19	ax-mp	⊢ ( 𝐹 : ( 𝐾 ∪ { 1 , 𝑀 } ) –1-1-onto→ ( 𝐾 ∪ { 1 , 𝑀 } ) ↔ ( 𝐺 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 𝐾 ∪ { 1 , 𝑀 } ) –1-1-onto→ ( 𝐾 ∪ { 1 , 𝑀 } ) )
21		f1oeq2	⊢ ( ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) → ( 𝐹 : ( 𝐾 ∪ { 1 , 𝑀 } ) –1-1-onto→ ( 𝐾 ∪ { 1 , 𝑀 } ) ↔ 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 𝐾 ∪ { 1 , 𝑀 } ) ) )
22	20 21	bitr3id	⊢ ( ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) → ( ( 𝐺 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 𝐾 ∪ { 1 , 𝑀 } ) –1-1-onto→ ( 𝐾 ∪ { 1 , 𝑀 } ) ↔ 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 𝐾 ∪ { 1 , 𝑀 } ) ) )
23		f1oeq3	⊢ ( ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) → ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 𝐾 ∪ { 1 , 𝑀 } ) ↔ 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
24	22 23	bitrd	⊢ ( ( 𝐾 ∪ { 1 , 𝑀 } ) = ( 1 ... ( 𝑁 + 1 ) ) → ( ( 𝐺 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 𝐾 ∪ { 1 , 𝑀 } ) –1-1-onto→ ( 𝐾 ∪ { 1 , 𝑀 } ) ↔ 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
25	18 24	syl	⊢ ( 𝜑 → ( ( 𝐺 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ) : ( 𝐾 ∪ { 1 , 𝑀 } ) –1-1-onto→ ( 𝐾 ∪ { 1 , 𝑀 } ) ↔ 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ) )
26	17 25	mpbid	⊢ ( 𝜑 → 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
27		f1ofun	⊢ ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → Fun 𝐹 )
28	26 27	syl	⊢ ( 𝜑 → Fun 𝐹 )
29		snsspr1	⊢ { ⟨ 1 , 𝑀 ⟩ } ⊆ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ }
30		ssun2	⊢ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ⊆ ( 𝐺 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } )
31	30 8	sseqtrri	⊢ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } ⊆ 𝐹
32	29 31	sstri	⊢ { ⟨ 1 , 𝑀 ⟩ } ⊆ 𝐹
33		1ex	⊢ 1 ∈ V
34	33	snid	⊢ 1 ∈ { 1 }
35	6	dmsnop	⊢ dom { ⟨ 1 , 𝑀 ⟩ } = { 1 }
36	34 35	eleqtrri	⊢ 1 ∈ dom { ⟨ 1 , 𝑀 ⟩ }
37		funssfv	⊢ ( ( Fun 𝐹 ∧ { ⟨ 1 , 𝑀 ⟩ } ⊆ 𝐹 ∧ 1 ∈ dom { ⟨ 1 , 𝑀 ⟩ } ) → ( 𝐹 ‘ 1 ) = ( { ⟨ 1 , 𝑀 ⟩ } ‘ 1 ) )
38	32 36 37	mp3an23	⊢ ( Fun 𝐹 → ( 𝐹 ‘ 1 ) = ( { ⟨ 1 , 𝑀 ⟩ } ‘ 1 ) )
39	28 38	syl	⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( { ⟨ 1 , 𝑀 ⟩ } ‘ 1 ) )
40	33 6	fvsn	⊢ ( { ⟨ 1 , 𝑀 ⟩ } ‘ 1 ) = 𝑀
41	39 40	eqtrdi	⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = 𝑀 )
42		snsspr2	⊢ { ⟨ 𝑀 , 1 ⟩ } ⊆ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ }
43	42 31	sstri	⊢ { ⟨ 𝑀 , 1 ⟩ } ⊆ 𝐹
44	6	snid	⊢ 𝑀 ∈ { 𝑀 }
45	33	dmsnop	⊢ dom { ⟨ 𝑀 , 1 ⟩ } = { 𝑀 }
46	44 45	eleqtrri	⊢ 𝑀 ∈ dom { ⟨ 𝑀 , 1 ⟩ }
47		funssfv	⊢ ( ( Fun 𝐹 ∧ { ⟨ 𝑀 , 1 ⟩ } ⊆ 𝐹 ∧ 𝑀 ∈ dom { ⟨ 𝑀 , 1 ⟩ } ) → ( 𝐹 ‘ 𝑀 ) = ( { ⟨ 𝑀 , 1 ⟩ } ‘ 𝑀 ) )
48	43 46 47	mp3an23	⊢ ( Fun 𝐹 → ( 𝐹 ‘ 𝑀 ) = ( { ⟨ 𝑀 , 1 ⟩ } ‘ 𝑀 ) )
49	28 48	syl	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) = ( { ⟨ 𝑀 , 1 ⟩ } ‘ 𝑀 ) )
50	6 33	fvsn	⊢ ( { ⟨ 𝑀 , 1 ⟩ } ‘ 𝑀 ) = 1
51	49 50	eqtrdi	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) = 1 )
52	26 41 51	3jca	⊢ ( 𝜑 → ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( 𝐹 ‘ 1 ) = 𝑀 ∧ ( 𝐹 ‘ 𝑀 ) = 1 ) )