Theorem f1opwfi 8153

Description: A one-to-one mapping induces a one-to-one mapping on finite subsets. (Contributed by Mario Carneiro, 25-Jan-2015.)

Assertion

Ref	Expression
f1opwfi	⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐹 “ 𝑏)):(𝒫 𝐴 ∩ Fin)–1-1-onto→(𝒫 𝐵 ∩ Fin))

Distinct variable groups:   𝐴,𝑏   𝐵,𝑏   𝐹,𝑏

Proof of Theorem f1opwfi

Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2610	. 2 ⊢ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐹 “ 𝑏)) = (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐹 “ 𝑏))
2		imassrn 5396	. . . . . 6 ⊢ (𝐹 “ 𝑏) ⊆ ran 𝐹
3		f1ofo 6057	. . . . . . 7 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)
4		forn 6031	. . . . . . 7 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
5	3, 4	syl 17	. . . . . 6 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ran 𝐹 = 𝐵)
6	2, 5	syl5sseq 3616	. . . . 5 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 “ 𝑏) ⊆ 𝐵)
7	6	adantr 480	. . . 4 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ 𝑏) ⊆ 𝐵)
8		inss2 3796	. . . . . . 7 ⊢ (𝒫 𝐴 ∩ Fin) ⊆ Fin
9		simpr 476	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑏 ∈ (𝒫 𝐴 ∩ Fin))
10	8, 9	sseldi 3566	. . . . . 6 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑏 ∈ Fin)
11		f1ofun 6052	. . . . . . . 8 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹)
12	11	adantr 480	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → Fun 𝐹)
13		inss1 3795	. . . . . . . . . . 11 ⊢ (𝒫 𝐴 ∩ Fin) ⊆ 𝒫 𝐴
14	13	sseli 3564	. . . . . . . . . 10 ⊢ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) → 𝑏 ∈ 𝒫 𝐴)
15		elpwi 4117	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝒫 𝐴 → 𝑏 ⊆ 𝐴)
16	14, 15	syl 17	. . . . . . . . 9 ⊢ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) → 𝑏 ⊆ 𝐴)
17	16	adantl 481	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑏 ⊆ 𝐴)
18		f1odm 6054	. . . . . . . . 9 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)
19	18	adantr 480	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → dom 𝐹 = 𝐴)
20	17, 19	sseqtr4d 3605	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑏 ⊆ dom 𝐹)
21		fores 6037	. . . . . . 7 ⊢ ((Fun 𝐹 ∧ 𝑏 ⊆ dom 𝐹) → (𝐹 ↾ 𝑏):𝑏–onto→(𝐹 “ 𝑏))
22	12, 20, 21	syl2anc 691	. . . . . 6 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑏):𝑏–onto→(𝐹 “ 𝑏))
23		fofi 8135	. . . . . 6 ⊢ ((𝑏 ∈ Fin ∧ (𝐹 ↾ 𝑏):𝑏–onto→(𝐹 “ 𝑏)) → (𝐹 “ 𝑏) ∈ Fin)
24	10, 22, 23	syl2anc 691	. . . . 5 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ 𝑏) ∈ Fin)
25		elpwg 4116	. . . . 5 ⊢ ((𝐹 “ 𝑏) ∈ Fin → ((𝐹 “ 𝑏) ∈ 𝒫 𝐵 ↔ (𝐹 “ 𝑏) ⊆ 𝐵))
26	24, 25	syl 17	. . . 4 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 “ 𝑏) ∈ 𝒫 𝐵 ↔ (𝐹 “ 𝑏) ⊆ 𝐵))
27	7, 26	mpbird 246	. . 3 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ 𝑏) ∈ 𝒫 𝐵)
28	27, 24	elind 3760	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑏 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 “ 𝑏) ∈ (𝒫 𝐵 ∩ Fin))
29		imassrn 5396	. . . . . 6 ⊢ (◡𝐹 “ 𝑎) ⊆ ran ◡𝐹
30		dfdm4 5238	. . . . . . 7 ⊢ dom 𝐹 = ran ◡𝐹
31	30, 18	syl5eqr 2658	. . . . . 6 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ran ◡𝐹 = 𝐴)
32	29, 31	syl5sseq 3616	. . . . 5 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 “ 𝑎) ⊆ 𝐴)
33	32	adantr 480	. . . 4 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (◡𝐹 “ 𝑎) ⊆ 𝐴)
34		inss2 3796	. . . . . . 7 ⊢ (𝒫 𝐵 ∩ Fin) ⊆ Fin
35		simpr 476	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ∈ (𝒫 𝐵 ∩ Fin))
36	34, 35	sseldi 3566	. . . . . 6 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ∈ Fin)
37		dff1o3 6056	. . . . . . . . 9 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))
38	37	simprbi 479	. . . . . . . 8 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun ◡𝐹)
39	38	adantr 480	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → Fun ◡𝐹)
40		inss1 3795	. . . . . . . . . . 11 ⊢ (𝒫 𝐵 ∩ Fin) ⊆ 𝒫 𝐵
41	40	sseli 3564	. . . . . . . . . 10 ⊢ (𝑎 ∈ (𝒫 𝐵 ∩ Fin) → 𝑎 ∈ 𝒫 𝐵)
42	41	adantl 481	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ∈ 𝒫 𝐵)
43		elpwi 4117	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵)
44	42, 43	syl 17	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ⊆ 𝐵)
45		f1ocnv 6062	. . . . . . . . . 10 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
46	45	adantr 480	. . . . . . . . 9 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → ◡𝐹:𝐵–1-1-onto→𝐴)
47		f1odm 6054	. . . . . . . . 9 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → dom ◡𝐹 = 𝐵)
48	46, 47	syl 17	. . . . . . . 8 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → dom ◡𝐹 = 𝐵)
49	44, 48	sseqtr4d 3605	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ⊆ dom ◡𝐹)
50		fores 6037	. . . . . . 7 ⊢ ((Fun ◡𝐹 ∧ 𝑎 ⊆ dom ◡𝐹) → (◡𝐹 ↾ 𝑎):𝑎–onto→(◡𝐹 “ 𝑎))
51	39, 49, 50	syl2anc 691	. . . . . 6 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (◡𝐹 ↾ 𝑎):𝑎–onto→(◡𝐹 “ 𝑎))
52		fofi 8135	. . . . . 6 ⊢ ((𝑎 ∈ Fin ∧ (◡𝐹 ↾ 𝑎):𝑎–onto→(◡𝐹 “ 𝑎)) → (◡𝐹 “ 𝑎) ∈ Fin)
53	36, 51, 52	syl2anc 691	. . . . 5 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (◡𝐹 “ 𝑎) ∈ Fin)
54		elpwg 4116	. . . . 5 ⊢ ((◡𝐹 “ 𝑎) ∈ Fin → ((◡𝐹 “ 𝑎) ∈ 𝒫 𝐴 ↔ (◡𝐹 “ 𝑎) ⊆ 𝐴))
55	53, 54	syl 17	. . . 4 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → ((◡𝐹 “ 𝑎) ∈ 𝒫 𝐴 ↔ (◡𝐹 “ 𝑎) ⊆ 𝐴))
56	33, 55	mpbird 246	. . 3 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (◡𝐹 “ 𝑎) ∈ 𝒫 𝐴)
57	56, 53	elind 3760	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (◡𝐹 “ 𝑎) ∈ (𝒫 𝐴 ∩ Fin))
58	14, 41	anim12i 588	. . 3 ⊢ ((𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵))
59	43	adantl 481	. . . . . . 7 ⊢ ((𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵) → 𝑎 ⊆ 𝐵)
60		foimacnv 6067	. . . . . . 7 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑎 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝑎)) = 𝑎)
61	3, 59, 60	syl2an 493	. . . . . 6 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → (𝐹 “ (◡𝐹 “ 𝑎)) = 𝑎)
62	61	eqcomd 2616	. . . . 5 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → 𝑎 = (𝐹 “ (◡𝐹 “ 𝑎)))
63		imaeq2 5381	. . . . . 6 ⊢ (𝑏 = (◡𝐹 “ 𝑎) → (𝐹 “ 𝑏) = (𝐹 “ (◡𝐹 “ 𝑎)))
64	63	eqeq2d 2620	. . . . 5 ⊢ (𝑏 = (◡𝐹 “ 𝑎) → (𝑎 = (𝐹 “ 𝑏) ↔ 𝑎 = (𝐹 “ (◡𝐹 “ 𝑎))))
65	62, 64	syl5ibrcom 236	. . . 4 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → (𝑏 = (◡𝐹 “ 𝑎) → 𝑎 = (𝐹 “ 𝑏)))
66		f1of1 6049	. . . . . . 7 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)
67	15	adantr 480	. . . . . . 7 ⊢ ((𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵) → 𝑏 ⊆ 𝐴)
68		f1imacnv 6066	. . . . . . 7 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑏 ⊆ 𝐴) → (◡𝐹 “ (𝐹 “ 𝑏)) = 𝑏)
69	66, 67, 68	syl2an 493	. . . . . 6 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → (◡𝐹 “ (𝐹 “ 𝑏)) = 𝑏)
70	69	eqcomd 2616	. . . . 5 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → 𝑏 = (◡𝐹 “ (𝐹 “ 𝑏)))
71		imaeq2 5381	. . . . . 6 ⊢ (𝑎 = (𝐹 “ 𝑏) → (◡𝐹 “ 𝑎) = (◡𝐹 “ (𝐹 “ 𝑏)))
72	71	eqeq2d 2620	. . . . 5 ⊢ (𝑎 = (𝐹 “ 𝑏) → (𝑏 = (◡𝐹 “ 𝑎) ↔ 𝑏 = (◡𝐹 “ (𝐹 “ 𝑏))))
73	70, 72	syl5ibrcom 236	. . . 4 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → (𝑎 = (𝐹 “ 𝑏) → 𝑏 = (◡𝐹 “ 𝑎)))
74	65, 73	impbid 201	. . 3 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ 𝒫 𝐴 ∧ 𝑎 ∈ 𝒫 𝐵)) → (𝑏 = (◡𝐹 “ 𝑎) ↔ 𝑎 = (𝐹 “ 𝑏)))
75	58, 74	sylan2 490	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑎 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑏 = (◡𝐹 “ 𝑎) ↔ 𝑎 = (𝐹 “ 𝑏)))
76	1, 28, 57, 75	f1o2d 6785	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝑏 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐹 “ 𝑏)):(𝒫 𝐴 ∩ Fin)–1-1-onto→(𝒫 𝐵 ∩ Fin))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ∩ cin 3539   ⊆ wss 3540  𝒫 cpw 4108   ↦ cmpt 4643  ^◡ccnv 5037  dom cdm 5038  ran crn 5039   ↾ cres 5040   “ cima 5041  Fun wfun 5798  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803  Fincfn 7841

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-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

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-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  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-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-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-om 6958  df-1o 7447  df-er 7629  df-en 7842  df-dom 7843  df-fin 7845

This theorem is referenced by:  fictb  8950  ackbijnn  14399  tsmsf1o  21758  eulerpartgbij  29761