Metamath Proof Explorer


Theorem pwfilemOLD

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

Ref Expression
Hypothesis pwfilemOLD.1 F = c 𝒫 b c x
Assertion pwfilemOLD 𝒫 b Fin 𝒫 b x Fin

Proof

Step Hyp Ref Expression
1 pwfilemOLD.1 F = c 𝒫 b c x
2 pwundif 𝒫 b x = 𝒫 b x 𝒫 b 𝒫 b
3 vex c V
4 snex x V
5 3 4 unex c x V
6 5 1 fnmpti F Fn 𝒫 b
7 dffn4 F Fn 𝒫 b F : 𝒫 b onto ran F
8 6 7 mpbi F : 𝒫 b onto ran F
9 fodomfi 𝒫 b Fin F : 𝒫 b onto ran F ran F 𝒫 b
10 8 9 mpan2 𝒫 b Fin ran F 𝒫 b
11 domfi 𝒫 b Fin ran F 𝒫 b ran F Fin
12 10 11 mpdan 𝒫 b Fin ran F Fin
13 eldifi d 𝒫 b x 𝒫 b d 𝒫 b x
14 4 elpwun d 𝒫 b x d x 𝒫 b
15 13 14 sylib d 𝒫 b x 𝒫 b d x 𝒫 b
16 undif1 d x x = d x
17 elpwunsn d 𝒫 b x 𝒫 b x d
18 17 snssd d 𝒫 b x 𝒫 b x d
19 ssequn2 x d d x = d
20 18 19 sylib d 𝒫 b x 𝒫 b d x = d
21 16 20 eqtr2id d 𝒫 b x 𝒫 b d = d x x
22 uneq1 c = d x c x = d x x
23 22 rspceeqv d x 𝒫 b d = d x x c 𝒫 b d = c x
24 15 21 23 syl2anc d 𝒫 b x 𝒫 b c 𝒫 b d = c x
25 1 5 elrnmpti d ran F c 𝒫 b d = c x
26 24 25 sylibr d 𝒫 b x 𝒫 b d ran F
27 26 ssriv 𝒫 b x 𝒫 b ran F
28 ssdomg ran F Fin 𝒫 b x 𝒫 b ran F 𝒫 b x 𝒫 b ran F
29 12 27 28 mpisyl 𝒫 b Fin 𝒫 b x 𝒫 b ran F
30 domfi ran F Fin 𝒫 b x 𝒫 b ran F 𝒫 b x 𝒫 b Fin
31 12 29 30 syl2anc 𝒫 b Fin 𝒫 b x 𝒫 b Fin
32 unfi 𝒫 b x 𝒫 b Fin 𝒫 b Fin 𝒫 b x 𝒫 b 𝒫 b Fin
33 31 32 mpancom 𝒫 b Fin 𝒫 b x 𝒫 b 𝒫 b Fin
34 2 33 eqeltrid 𝒫 b Fin 𝒫 b x Fin