Theorem subfacp1lem4 30419

Description: Lemma for subfacp1 30422. The function 𝐹, which swaps 1 with 𝑀 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.)

Hypotheses

Ref	Expression
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

Ref	Expression
subfacp1lem4	⊢ (𝜑 → ◡𝐹 = 𝐹)

Distinct variable groups:   𝑓,𝑔,𝑛,𝑥,𝑦,𝐴   𝑓,𝐹,𝑔,𝑥,𝑦   𝑓,𝑁,𝑔,𝑛,𝑥,𝑦   𝐵,𝑓,𝑔,𝑥,𝑦   𝜑,𝑥,𝑦   𝐷,𝑛   𝑓,𝐾,𝑛,𝑥,𝑦   𝑓,𝑀,𝑔,𝑥,𝑦   𝑆,𝑛,𝑥,𝑦

Allowed substitution hints:   𝜑(𝑓,𝑔,𝑛)   𝐵(𝑛)   𝐷(𝑥,𝑦,𝑓,𝑔)   𝑆(𝑓,𝑔)   𝐹(𝑛)   𝐾(𝑔)   𝑀(𝑛)

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 6086	. . . . . 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 30416	. . . 4 ⊢ (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹‘𝑀) = 1))
12	11	simp1d 1066	. . 3 ⊢ (𝜑 → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
13		f1ocnv 6062	. . 3 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ◡𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
14		f1ofn 6051	. . 3 ⊢ (◡𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → ◡𝐹 Fn (1...(𝑁 + 1)))
15	12, 13, 14	3syl 18	. 2 ⊢ (𝜑 → ◡𝐹 Fn (1...(𝑁 + 1)))
16		f1ofn 6051	. . 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 30415	. . . . . . . 8 ⊢ (𝜑 → ((𝐾 ∩ {1, 𝑀}) = ∅ ∧ (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) ∧ (#‘𝐾) = (𝑁 − 1)))
19	18	simp2d 1067	. . . . . . 7 ⊢ (𝜑 → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)))
20	19	eleq2d 2673	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝐾 ∪ {1, 𝑀}) ↔ 𝑥 ∈ (1...(𝑁 + 1))))
21	20	biimpar 501	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝑁 + 1))) → 𝑥 ∈ (𝐾 ∪ {1, 𝑀}))
22		elun 3715	. . . . 5 ⊢ (𝑥 ∈ (𝐾 ∪ {1, 𝑀}) ↔ (𝑥 ∈ 𝐾 ∨ 𝑥 ∈ {1, 𝑀}))
23	21, 22	sylib 207	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝑁 + 1))) → (𝑥 ∈ 𝐾 ∨ 𝑥 ∈ {1, 𝑀}))
24	1, 2, 3, 4, 5, 6, 7, 8, 10	subfacp1lem2b 30417	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐹‘𝑥) = (( I ↾ 𝐾)‘𝑥))
25		fvresi 6344	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐾 → (( I ↾ 𝐾)‘𝑥) = 𝑥)
26	25	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (( I ↾ 𝐾)‘𝑥) = 𝑥)
27	24, 26	eqtrd 2644	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐹‘𝑥) = 𝑥)
28	27	fveq2d 6107	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐹‘(𝐹‘𝑥)) = (𝐹‘𝑥))
29	28, 27	eqtrd 2644	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐹‘(𝐹‘𝑥)) = 𝑥)
30		vex 3176	. . . . . . 7 ⊢ 𝑥 ∈ V
31	30	elpr 4146	. . . . . 6 ⊢ (𝑥 ∈ {1, 𝑀} ↔ (𝑥 = 1 ∨ 𝑥 = 𝑀))
32	11	simp2d 1067	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘1) = 𝑀)
33	32	fveq2d 6107	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘(𝐹‘1)) = (𝐹‘𝑀))
34	11	simp3d 1068	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝑀) = 1)
35	33, 34	eqtrd 2644	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝐹‘1)) = 1)
36		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1))
37	36	fveq2d 6107	. . . . . . . . . 10 ⊢ (𝑥 = 1 → (𝐹‘(𝐹‘𝑥)) = (𝐹‘(𝐹‘1)))
38		id 22	. . . . . . . . . 10 ⊢ (𝑥 = 1 → 𝑥 = 1)
39	37, 38	eqeq12d 2625	. . . . . . . . 9 ⊢ (𝑥 = 1 → ((𝐹‘(𝐹‘𝑥)) = 𝑥 ↔ (𝐹‘(𝐹‘1)) = 1))
40	35, 39	syl5ibrcom 236	. . . . . . . 8 ⊢ (𝜑 → (𝑥 = 1 → (𝐹‘(𝐹‘𝑥)) = 𝑥))
41	34	fveq2d 6107	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘(𝐹‘𝑀)) = (𝐹‘1))
42	41, 32	eqtrd 2644	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘(𝐹‘𝑀)) = 𝑀)
43		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑀 → (𝐹‘𝑥) = (𝐹‘𝑀))
44	43	fveq2d 6107	. . . . . . . . . 10 ⊢ (𝑥 = 𝑀 → (𝐹‘(𝐹‘𝑥)) = (𝐹‘(𝐹‘𝑀)))
45		id 22	. . . . . . . . . 10 ⊢ (𝑥 = 𝑀 → 𝑥 = 𝑀)
46	44, 45	eqeq12d 2625	. . . . . . . . 9 ⊢ (𝑥 = 𝑀 → ((𝐹‘(𝐹‘𝑥)) = 𝑥 ↔ (𝐹‘(𝐹‘𝑀)) = 𝑀))
47	42, 46	syl5ibrcom 236	. . . . . . . 8 ⊢ (𝜑 → (𝑥 = 𝑀 → (𝐹‘(𝐹‘𝑥)) = 𝑥))
48	40, 47	jaod 394	. . . . . . 7 ⊢ (𝜑 → ((𝑥 = 1 ∨ 𝑥 = 𝑀) → (𝐹‘(𝐹‘𝑥)) = 𝑥))
49	48	imp 444	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 = 1 ∨ 𝑥 = 𝑀)) → (𝐹‘(𝐹‘𝑥)) = 𝑥)
50	31, 49	sylan2b 491	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {1, 𝑀}) → (𝐹‘(𝐹‘𝑥)) = 𝑥)
51	29, 50	jaodan 822	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∨ 𝑥 ∈ {1, 𝑀})) → (𝐹‘(𝐹‘𝑥)) = 𝑥)
52	23, 51	syldan 486	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝑁 + 1))) → (𝐹‘(𝐹‘𝑥)) = 𝑥)
53	12	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝑁 + 1))) → 𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)))
54		f1of 6050	. . . . . 6 ⊢ (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
55	12, 54	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
56	55	ffvelrnda 6267	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝑁 + 1))) → (𝐹‘𝑥) ∈ (1...(𝑁 + 1)))
57		f1ocnvfv 6434	. . . 4 ⊢ ((𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘𝑥) ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝐹‘𝑥)) = 𝑥 → (◡𝐹‘𝑥) = (𝐹‘𝑥)))
58	53, 56, 57	syl2anc 691	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝑁 + 1))) → ((𝐹‘(𝐹‘𝑥)) = 𝑥 → (◡𝐹‘𝑥) = (𝐹‘𝑥)))
59	52, 58	mpd 15	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(𝑁 + 1))) → (◡𝐹‘𝑥) = (𝐹‘𝑥))
60	15, 17, 59	eqfnfvd 6222	1 ⊢ (𝜑 → ◡𝐹 = 𝐹)

Syntax hints:   → wi 4   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539  ∅c0 3874  {csn 4125  {cpr 4127  ⟨cop 4131   ↦ cmpt 4643   I cid 4948  ^◡ccnv 5037   ↾ cres 5040   Fn wfn 5799  ⟶wf 5800  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549  Fincfn 7841  1c1 9816   + caddc 9818   − cmin 10145  ℕcn 10897  2c2 10947  ℕ₀cn0 11169  ...cfz 12197  #chash 12979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-hash 12980

This theorem is referenced by:  subfacp1lem5  30420