Theorem subfacp1lem2b

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	subfacp1lem2b	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )

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	1 2 3 4 5 6 7 8 9	subfacp1lem2a	⊢ ( 𝜑 → ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ( 𝐹 ‘ 1 ) = 𝑀 ∧ ( 𝐹 ‘ 𝑀 ) = 1 ) )
11	10	simp1d	⊢ ( 𝜑 → 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) )
12		f1ofun	⊢ ( 𝐹 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) → Fun 𝐹 )
13	11 12	syl	⊢ ( 𝜑 → Fun 𝐹 )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ) → Fun 𝐹 )
15		ssun1	⊢ 𝐺 ⊆ ( 𝐺 ∪ { ⟨ 1 , 𝑀 ⟩ , ⟨ 𝑀 , 1 ⟩ } )
16	15 8	sseqtrri	⊢ 𝐺 ⊆ 𝐹
17	16	a1i	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ) → 𝐺 ⊆ 𝐹 )
18		f1odm	⊢ ( 𝐺 : 𝐾 –1-1-onto→ 𝐾 → dom 𝐺 = 𝐾 )
19	9 18	syl	⊢ ( 𝜑 → dom 𝐺 = 𝐾 )
20	19	eleq2d	⊢ ( 𝜑 → ( 𝑋 ∈ dom 𝐺 ↔ 𝑋 ∈ 𝐾 ) )
21	20	biimpar	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ) → 𝑋 ∈ dom 𝐺 )
22		funssfv	⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ∧ 𝑋 ∈ dom 𝐺 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )
23	14 17 21 22	syl3anc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑋 ) )