Theorem pwfilemOLD 9342

Description: Obsolete version of pwfilem 9173 as of 7-Sep-2024. (Contributed by NM, 26-Mar-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
pwfilemOLD.1	⊢ 𝐹 = (𝑐 ∈ 𝒫 𝑏 ↦ (𝑐 ∪ {𝑥}))

Assertion

Ref	Expression
pwfilemOLD	⊢ (𝒫 𝑏 ∈ Fin → 𝒫 (𝑏 ∪ {𝑥}) ∈ Fin)

Distinct variable groups:   𝑏,𝑐   𝑥,𝑐

Allowed substitution hints:   𝐹(𝑥,𝑏,𝑐)

Proof of Theorem pwfilemOLD

Dummy variable 𝑑 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pwundif 4625	. 2 ⊢ 𝒫 (𝑏 ∪ {𝑥}) = ((𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ∪ 𝒫 𝑏)
2		vex 3479	. . . . . . . . 9 ⊢ 𝑐 ∈ V
3		snex 5430	. . . . . . . . 9 ⊢ {𝑥} ∈ V
4	2, 3	unex 7728	. . . . . . . 8 ⊢ (𝑐 ∪ {𝑥}) ∈ V
5		pwfilemOLD.1	. . . . . . . 8 ⊢ 𝐹 = (𝑐 ∈ 𝒫 𝑏 ↦ (𝑐 ∪ {𝑥}))
6	4, 5	fnmpti 6690	. . . . . . 7 ⊢ 𝐹 Fn 𝒫 𝑏
7		dffn4 6808	. . . . . . 7 ⊢ (𝐹 Fn 𝒫 𝑏 ↔ 𝐹:𝒫 𝑏–onto→ran 𝐹)
8	6, 7	mpbi 229	. . . . . 6 ⊢ 𝐹:𝒫 𝑏–onto→ran 𝐹
9		fodomfi 9321	. . . . . 6 ⊢ ((𝒫 𝑏 ∈ Fin ∧ 𝐹:𝒫 𝑏–onto→ran 𝐹) → ran 𝐹 ≼ 𝒫 𝑏)
10	8, 9	mpan2 690	. . . . 5 ⊢ (𝒫 𝑏 ∈ Fin → ran 𝐹 ≼ 𝒫 𝑏)
11		domfi 9188	. . . . 5 ⊢ ((𝒫 𝑏 ∈ Fin ∧ ran 𝐹 ≼ 𝒫 𝑏) → ran 𝐹 ∈ Fin)
12	10, 11	mpdan 686	. . . 4 ⊢ (𝒫 𝑏 ∈ Fin → ran 𝐹 ∈ Fin)
13		eldifi 4125	. . . . . . . . 9 ⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → 𝑑 ∈ 𝒫 (𝑏 ∪ {𝑥}))
14	3	elpwun 7751	. . . . . . . . 9 ⊢ (𝑑 ∈ 𝒫 (𝑏 ∪ {𝑥}) ↔ (𝑑 ∖ {𝑥}) ∈ 𝒫 𝑏)
15	13, 14	sylib 217	. . . . . . . 8 ⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → (𝑑 ∖ {𝑥}) ∈ 𝒫 𝑏)
16		undif1 4474	. . . . . . . . 9 ⊢ ((𝑑 ∖ {𝑥}) ∪ {𝑥}) = (𝑑 ∪ {𝑥})
17		elpwunsn 4686	. . . . . . . . . . 11 ⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → 𝑥 ∈ 𝑑)
18	17	snssd 4811	. . . . . . . . . 10 ⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → {𝑥} ⊆ 𝑑)
19		ssequn2 4182	. . . . . . . . . 10 ⊢ ({𝑥} ⊆ 𝑑 ↔ (𝑑 ∪ {𝑥}) = 𝑑)
20	18, 19	sylib 217	. . . . . . . . 9 ⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → (𝑑 ∪ {𝑥}) = 𝑑)
21	16, 20	eqtr2id 2786	. . . . . . . 8 ⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → 𝑑 = ((𝑑 ∖ {𝑥}) ∪ {𝑥}))
22		uneq1 4155	. . . . . . . . 9 ⊢ (𝑐 = (𝑑 ∖ {𝑥}) → (𝑐 ∪ {𝑥}) = ((𝑑 ∖ {𝑥}) ∪ {𝑥}))
23	22	rspceeqv 3632	. . . . . . . 8 ⊢ (((𝑑 ∖ {𝑥}) ∈ 𝒫 𝑏 ∧ 𝑑 = ((𝑑 ∖ {𝑥}) ∪ {𝑥})) → ∃𝑐 ∈ 𝒫 𝑏𝑑 = (𝑐 ∪ {𝑥}))
24	15, 21, 23	syl2anc 585	. . . . . . 7 ⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → ∃𝑐 ∈ 𝒫 𝑏𝑑 = (𝑐 ∪ {𝑥}))
25	5, 4	elrnmpti 5957	. . . . . . 7 ⊢ (𝑑 ∈ ran 𝐹 ↔ ∃𝑐 ∈ 𝒫 𝑏𝑑 = (𝑐 ∪ {𝑥}))
26	24, 25	sylibr 233	. . . . . 6 ⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → 𝑑 ∈ ran 𝐹)
27	26	ssriv 3985	. . . . 5 ⊢ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ⊆ ran 𝐹
28		ssdomg 8992	. . . . 5 ⊢ (ran 𝐹 ∈ Fin → ((𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ⊆ ran 𝐹 → (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ≼ ran 𝐹))
29	12, 27, 28	mpisyl 21	. . . 4 ⊢ (𝒫 𝑏 ∈ Fin → (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ≼ ran 𝐹)
30		domfi 9188	. . . 4 ⊢ ((ran 𝐹 ∈ Fin ∧ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ≼ ran 𝐹) → (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ∈ Fin)
31	12, 29, 30	syl2anc 585	. . 3 ⊢ (𝒫 𝑏 ∈ Fin → (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ∈ Fin)
32		unfi 9168	. . 3 ⊢ (((𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ∈ Fin ∧ 𝒫 𝑏 ∈ Fin) → ((𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ∪ 𝒫 𝑏) ∈ Fin)
33	31, 32	mpancom 687	. 2 ⊢ (𝒫 𝑏 ∈ Fin → ((𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ∪ 𝒫 𝑏) ∈ Fin)
34	1, 33	eqeltrid 2838	1 ⊢ (𝒫 𝑏 ∈ Fin → 𝒫 (𝑏 ∪ {𝑥}) ∈ Fin)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  ∃wrex 3071   ∖ cdif 3944   ∪ cun 3945   ⊆ wss 3947  𝒫 cpw 4601  {csn 4627   class class class wbr 5147   ↦ cmpt 5230  ran crn 5676   Fn wfn 6535  –onto→wfo 6538   ≼ cdom 8933  Fincfn 8935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-om 7851  df-1o 8461  df-er 8699  df-en 8936  df-dom 8937  df-fin 8939

This theorem is referenced by: (None)